theory Detype_R

lemma cte_wp_at_modify_pde:
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows
  "\<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s;cte_wp_at' \<top> ptr s\<rbrakk>
       \<Longrightarrow> cte_wp_at' \<top> ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> (KOArch (KOPDE pde')))\<rparr>)" apply (simp add:cte_wp_at_obj_cases_mask obj_at'_real_def) apply (frule(1) pspace_alignedD') apply (elim disjE) apply (rule disjI1) apply (clarsimp simp add:ko_wp_at'_def) apply (intro conjI impI) apply (simp add:objBits_simps archObjSize_def) apply (clarsimp simp:projectKO_opt_cte) apply (simp add:ps_clear_def)+ apply (clarsimp simp:objBits_simps archObjSize_def) apply (simp add:ps_clear_def) apply (rule ccontr) apply simp apply (erule in_emptyE, blast) apply simp apply (rule disjI2) apply (clarsimp simp:ko_wp_at'_def) apply (intro conjI impI) apply (simp add:objBits_simps archObjSize_def)+ apply (clarsimp simp:projectKO_opt_cte projectKO_opt_tcb) apply (simp add:ps_clear_def)+ apply (clarsimp simp:objBits_simps archObjSize_def) apply (simp add:ps_clear_def) apply (rule ccontr) apply simp apply (erule in_emptyE) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; cte_wp_at' (\<lambda>_. True) ptr s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr s \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr s \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde)))\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> (ptr = ptr' \<longrightarrow> is_aligned ptr' (objBitsKO (KOArch (KOPDE pde'))) \<and> (\<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj) \<and> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)) \<and> (ptr \<noteq> ptr' \<longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>))
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> is_aligned ptr' (objBitsKO (KOArch (KOPDE pde')))
 2. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj
 3. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 4. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 5. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj
 2. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 3. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 4. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 2. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 3. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some ko; pspace_aligned' s; KOArch (KOPDE pde) = ko; is_aligned ptr' (objBitsKO ko); ({ptr'..ptr' + 2 ^ objBitsKO ko - 1} - {ptr'}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr = ptr'\<rbrakk> \<Longrightarrow> ({ptr'..ptr' + 2 ^ objBitsKO (KOArch (KOPDE pde')) - 1} - {ptr'}) \<inter> dom (ksPSpace s) = {}
 2. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 3. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr \<noteq> ptr'\<rbrakk> \<Longrightarrow> ptr' \<notin> {ptr..ptr + 2 ^ objBitsKO ko - 1}
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr \<noteq> ptr'; \<not> ptr' \<notin> {ptr..ptr + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ({ptr..ptr + 2 ^ objBitsKO ko - 1} - {ptr}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr \<noteq> ptr'; ptr' \<in> {ptr..ptr + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) ptr (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) \<or> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); ptr && mask tcbBlockSizeBits \<in> dom tcb_cte_cases \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) (ptr && ~~ mask tcbBlockSizeBits) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> (ptr && ~~ mask tcbBlockSizeBits = ptr' \<longrightarrow> is_aligned ptr' (objBitsKO (KOArch (KOPDE pde'))) \<and> (\<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj) \<and> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)) \<and> (ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr' \<longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> is_aligned ptr' (objBitsKO (KOArch (KOPDE pde')))
 2. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj
 3. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 4. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some ko; pspace_aligned' s; is_aligned ptr' pdeBits; tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); KOArch (KOPDE pde) = ko; is_aligned ptr' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits); ps_clear ptr' (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch (KOPDE pde')) = Some obj
 2. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 3. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> ps_clear ptr' (objBitsKO (KOArch (KOPDE pde'))) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>)
 2. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some ko; pspace_aligned' s; tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); KOArch (KOPDE pde) = ko; is_aligned ptr' (objBitsKO ko); ({ptr'..ptr' + 2 ^ objBitsKO ko - 1} - {ptr'}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits = ptr'\<rbrakk> \<Longrightarrow> ({ptr'..ptr' + 2 ^ objBitsKO (KOArch (KOPDE pde')) - 1} - {ptr'}) \<inter> dom (ksPSpace s) = {}
 2. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) s; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ps_clear (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(ptr' \<mapsto> KOArch (KOPDE pde'))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ({ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1} - {ptr && ~~ mask tcbBlockSizeBits}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'\<rbrakk> \<Longrightarrow> ptr' \<notin> {ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1} proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ({ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1} - {ptr && ~~ mask tcbBlockSizeBits}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'; \<not> ptr' \<notin> {ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); ({ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1} - {ptr && ~~ mask tcbBlockSizeBits}) \<inter> dom (ksPSpace s) = {}; projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'; ptr' \<in> {ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko a b obj. \<lbrakk>ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s; is_aligned ptr' (objBitsKO (KOArch (KOPDE pde))); tcb_cte_cases (ptr && mask tcbBlockSizeBits) = Some (a, b); ksPSpace s (ptr && ~~ mask tcbBlockSizeBits) = Some ko; is_aligned (ptr && ~~ mask tcbBlockSizeBits) (objBitsKO ko); projectKO_opt ko = Some obj; ptr && ~~ mask tcbBlockSizeBits \<noteq> ptr'; ptr' \<in> {ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> ?x104 ko a b obj \<in> ({ptr && ~~ mask tcbBlockSizeBits..(ptr && ~~ mask tcbBlockSizeBits) + 2 ^ objBitsKO ko - 1} - {ptr && ~~ mask tcbBlockSizeBits}) \<inter> dom (ksPSpace s) proof (prove)
goal:
No subgoals!