theory CSpace1_R

lemma capFreeIndex_update_valid_cap':
  "\<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (of_nat fb :: word32) minUntypedSizeBits;
    s \<turnstile>' capability.UntypedCap d v bits fa\<rbrakk>
   \<Longrightarrow> s \<turnstile>' capability.UntypedCap d v bits fb" apply (clarsimp simp:valid_cap'_def capAligned_def valid_untyped'_def ko_wp_at'_def) apply (intro conjI impI allI) apply (elim allE) apply (erule(1) impE)+ apply (erule disjE) apply simp_all apply (rule disjI1) apply clarsimp apply (erule disjoint_subset2[rotated]) apply (clarsimp) apply (rule word_plus_mono_right) apply (rule of_nat_mono_maybe_le[THEN iffD1]) apply (subst word_bits_def[symmetric]) apply (erule less_le_trans[OF _  power_increasing]) apply simp apply simp apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply (erule less_le_trans[OF _ power_increasing]) apply simp+ apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply simp apply (erule allE)+ apply (erule(1) impE)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; valid_cap' (capability.UntypedCap d v bits fa) s\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap d v bits fb) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (fb < 2 ^ bits \<longrightarrow> (\<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s)) \<and> (fb = 2 ^ bits \<longrightarrow> (\<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko\<rbrakk> \<Longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; is_aligned (?ptr'33 ptr' ko) (objBitsKO (?ko34 ptr' ko)) \<longrightarrow> ksPSpace s (?ptr'33 ptr' ko) = Some (?ko34 ptr' ko) \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' (?ptr'33 ptr' ko) (?ko34 ptr' ko) \<and> obj_range' (?ptr'33 ptr' ko) (?ko34 ptr' ko) \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear (?ptr'33 ptr' ko) (objBitsKO (?ko34 ptr' ko)) s\<rbrakk> \<Longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {}\<rbrakk> \<Longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; fb \<le> 2 ^ bits; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fa..v + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> {v + word_of_nat fa..v + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {}
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; obj_range' ptr' ko \<inter> {v + word_of_nat fa..v + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {v + word_of_nat fb..v + 2 ^ bits - 1} = {}
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> {v + word_of_nat fb..v + 2 ^ bits - 1} \<subseteq> {v + word_of_nat fa..v + 2 ^ bits - 1}
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v + word_of_nat fa \<le> v + word_of_nat fb
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word_of_nat fa \<le> word_of_nat fb
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 3. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fb < 2 ^ LENGTH(32)
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ LENGTH(32)
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 5. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fb < 2 ^ word_bits
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ LENGTH(32)
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 5. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (6 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> bits \<le> word_bits
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ LENGTH(32)
 4. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 5. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 6. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ LENGTH(32)
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 5. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ LENGTH(32)
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa < 2 ^ word_bits
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (4 subgoals):
 1. \<And>ptr' ko. \<lbrakk>is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fb < 2 ^ word_bits
 2. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (5 subgoals):
 1. \<And>ptr' ko. \<lbrakk>is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> bits \<le> word_bits
 2. \<And>ptr' ko. \<lbrakk>is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fa \<le> fb
 4. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 5. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> v \<le> v + word_of_nat fb
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word_of_nat fb < 2 ^ bits
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> fb; is_aligned (word_of_nat fb) minUntypedSizeBits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb < 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; v + word_of_nat fb \<le> v + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> fb < unat (2 ^ bits)
 2. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; \<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; is_aligned (?ptr'84 ptr' ko) (objBitsKO (?ko86 ptr' ko)) \<longrightarrow> ksPSpace s (?ptr'84 ptr' ko) = Some (?ko86 ptr' ko) \<longrightarrow> \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' (?ptr'84 ptr' ko) (?ko86 ptr' ko) \<and> obj_range' (?ptr'84 ptr' ko) (?ko86 ptr' ko) \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear (?ptr'84 ptr' ko) (objBitsKO (?ko86 ptr' ko)) s\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>fa \<le> 2 ^ bits; is_aligned (2 ^ bits) minUntypedSizeBits; is_aligned v bits; bits < word_bits; v \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; is_aligned (word_of_nat fa) minUntypedSizeBits; fb = 2 ^ bits; is_aligned ptr' (objBitsKO ko); ksPSpace s ptr' = Some ko; {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko; \<not> {v..v + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> (if fa < 2 ^ bits then {v + word_of_nat fa..v + 2 ^ bits - 1} else {}) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<not> ps_clear ptr' (objBitsKO ko) s proof (prove)
goal:
No subgoals!