theory Detype_R

lemma createObjects'_pspace_no_overlap2:
  "\<lbrace>pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz
       and K (gz = (objBitsKO val) + us)
       and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace>
    createObjects' ptr (Suc n) val us
  \<lbrace>\<lambda>addrs s. pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz s\<rbrace>" proof - note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex show ?thesis apply (rule hoare_gen_asm)+ apply (clarsimp simp:createObjects'_def split_def new_cap_addrs_fold') apply (subst new_cap_addrs_fold') apply clarsimp apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (drule_tac gbits = us in range_cover_not_zero_shift[rotated]) apply simp+ apply (simp add:word_le_sub1) apply (wp haskell_assert_wp unless_wp |wpc
         |simp add:alignError_def del:fun_upd_apply)+ apply (rule conjI) apply (rule impI) apply (subgoal_tac
     "pspace_no_overlap' (ptr + (1 + of_nat n << objBitsKO val + us))
       sz
      (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val))
                     (new_cap_addrs (unat (1 + of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)") apply (intro conjI impI allI) apply assumption+ apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (subst (asm) foldr_upd_app_if) apply (subst range_cover_tail_mask) apply simp+ apply (clarsimp split:if_splits) apply (drule obj_range'_subset_strong[rotated]) apply (rule range_cover_rel[OF range_cover_le[where n = "Suc n"]],assumption) apply simp+ apply (drule range_cover.unat_of_nat_n_shift
       [OF range_cover_le[where n = "Suc n"],where gbits = us]) apply simp+ apply (simp add:shiftl_t2n field_simps)+ apply (simp add:obj_range'_def) apply (erule disjoint_subset) apply (clarsimp simp:blah) apply (thin_tac "x \<le> y" for x y) apply (subst (asm) le_m1_iff_lt[THEN iffD1]) apply (drule_tac range_cover_no_0[rotated,where p = "Suc n"]) apply simp apply simp apply (simp add:field_simps) apply (simp add: power_add[symmetric]) apply (simp add: word_neq_0_conv) apply (simp add: power_add[symmetric] field_simps) apply (frule range_cover_subset[where p = "Suc n"]) apply simp apply simp apply (drule(1) pspace_no_overlapD') apply (subst (asm) range_cover_tail_mask) apply simp+ apply (simp add:word_le_sub1 shiftl_t2n field_simps) apply auto done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz and K (gz = objBitsKO val + us) and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz and K (gz = objBitsKO val + us) and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> proof (state)
this:
untyped_range (cap.UntypedCap ?dev ?p ?n ?f) = {?p..?p + (1 << ?n) - 1}
untyped_range cap.NullCap = {}
untyped_range (cap.EndpointCap ?r ?badge ?rights) = {}
untyped_range (cap.NotificationCap ?r ?badge ?rights) = {}
untyped_range (cap.CNodeCap ?r ?bits ?guard) = {}
untyped_range (cap.ThreadCap ?r) = {}
untyped_range cap.DomainCap = {}
untyped_range (cap.ReplyCap ?r ?master ?rights) = {}
untyped_range cap.IRQControlCap = {}
untyped_range (cap.IRQHandlerCap ?irq) = {}
untyped_range (cap.Zombie ?r ?b ?n) = {}
untyped_range (cap.ArchObjectCap ?cap) = {}
usable_untyped_range (cap.UntypedCap ?uu ?p ?n ?f) = (if ?f < 2 ^ ?n then {?p + word_of_nat ?f..?p + 2 ^ ?n - 1} else {})
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz and K (gz = objBitsKO val + us) and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz and K (gz = objBitsKO val + us) and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0; gz = objBitsKO val + us\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (1 + word_of_nat n << us) - 1]) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>_ ya ps y a. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 2. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 2. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> Suc n \<le> Suc (Suc n)
 2. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; range_cover ptr sz (objBitsKO val + us) (Suc n)\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 3. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; range_cover ptr sz (objBitsKO val + us) (Suc n)\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 2. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> us \<le> objBitsKO val + us
 2. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> Suc n \<noteq> 0
 3. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; word_of_nat (Suc n) << us \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 4. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; 1 + word_of_nat n << us \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> 1 + word_of_nat n << us
 2. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> do y <- unless (ptr && mask (objBitsKO val + us) = 0) (alignError (objBitsKO val + us));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) ps))
od \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> (ptr && mask (objBitsKO val + us) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>))) \<and> (ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>))
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>))
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>))
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>); fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = None\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s a. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>); \<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO val + us) - Suc 0)) (ksPSpace s)) = Some (a, b); a < ptr\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>)
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> \<forall>x ko. ksPSpace (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>) x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; ksPSpace (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) (ksPSpace s)\<rparr>) x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; ksPSpace (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) then Some val else ksPSpace s x\<rparr>) x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; ksPSpace (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) then Some val else ksPSpace s x\<rparr>) x = Some ko\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val + us) (Suc (Suc n))
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; ksPSpace (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) then Some val else ksPSpace s x\<rparr>) x = Some ko\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; ksPSpace (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) then Some val else ksPSpace s x\<rparr>) x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; (if x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) then Some val else ksPSpace s x) = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<in> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> range_cover ptr (?sz92 s x) (objBitsKO val) (unat (1 + word_of_nat n << us))
 2. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> Suc n \<le> Suc (Suc n)
 2. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> objBitsKO val \<le> objBitsKO val + us
 3. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ (objBitsKO val + us - objBitsKO val) * Suc n
 4. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 5. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 6. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ us + 2 ^ us * n
 2. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> Suc n \<le> Suc (Suc n)
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0\<rbrakk> \<Longrightarrow> us \<le> objBitsKO val + us
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; unat (word_of_nat (Suc n) << us) = Suc n * 2 ^ us\<rbrakk> \<Longrightarrow> unat (1 + word_of_nat n << us) = 2 ^ us + 2 ^ us * n
 4. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; obj_range' x val \<subseteq> {ptr..ptr + word_of_nat (unat (1 + word_of_nat n << us)) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 5. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 6. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; obj_range' x val \<subseteq> {ptr..ptr + (1 + word_of_nat n << us) * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; obj_range' x val \<subseteq> {ptr..ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; {x..x + 2 ^ objBitsKO val - 1} \<subseteq> {ptr..ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO val - 1} \<inter> {ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0\<rbrakk> \<Longrightarrow> {ptr..ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1} \<inter> {ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val))
 2. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0\<rbrakk> \<Longrightarrow> Suc n < Suc (Suc n)
 2. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 3. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + word_of_nat (Suc n) * 2 ^ (us + objBitsKO val) \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val))
 4. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 5. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 6. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 2. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + word_of_nat (Suc n) * 2 ^ (us + objBitsKO val) \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val))
 3. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 4. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 5. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + word_of_nat (Suc n) * 2 ^ (us + objBitsKO val) \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val))
 2. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val))
 2. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>ptr \<le> ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; gz = us + objBitsKO val; ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))
 2. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>gz = us + objBitsKO val; range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val))) sz s; ptr && mask (us + objBitsKO val) = 0; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) < ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)); ptr \<le> ptr + (2 ^ us * 2 ^ objBitsKO val + word_of_nat n * (2 ^ us * 2 ^ objBitsKO val)) - 1; ptr + (2 ^ (us + objBitsKO val) + word_of_nat n * 2 ^ (us + objBitsKO val)) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> Suc n < Suc (Suc n)
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> Suc (Suc n) \<noteq> 0
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko; {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (3 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko\<rbrakk> \<Longrightarrow> Suc (Suc n) \<noteq> 0
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko; {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 3. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); ksPSpace s x = Some ko; {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr + (1 + word_of_nat n << objBitsKO val + us) && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (4 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val + us) (Suc (Suc n))
 2. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 3. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us)..ptr + word_of_nat (Suc n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc (Suc n)) * 2 ^ (objBitsKO val + us) - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 4. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s; ptr && mask (objBitsKO val + us) = 0; x \<notin> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val); {ptr + (1 + word_of_nat n) * 2 ^ (objBitsKO val + us)..ptr + (1 + word_of_nat n) * 2 ^ (objBitsKO val + us) + 2 ^ (objBitsKO val + us) - 1} \<subseteq> {ptr..ptr + (2 + word_of_nat n) * 2 ^ (objBitsKO val + us) - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {ptr + (1 + word_of_nat n << objBitsKO val + us)..(ptr && ~~ mask sz) + (2 ^ sz - 1)} = {}
 2. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>gz = objBitsKO val + us; range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); ptr \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << objBitsKO val + us)) sz s\<rbrakk> \<Longrightarrow> ptr && mask (objBitsKO val + us) \<noteq> 0 \<longrightarrow> ?Q40 s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz and K (gz = objBitsKO val + us) and K (range_cover ptr sz gz (Suc (Suc n)) \<and> ptr \<noteq> 0)\<rbrace> createObjects' ptr (Suc n) val us \<lbrace>\<lambda>addrs. pspace_no_overlap' (ptr + (1 + word_of_nat n << gz)) sz\<rbrace>

goal:
No subgoals!