theory ArchMove_C

lemma valid_untyped':
  notes usableUntypedRange.simps[simp del]
  assumes pspace_distinct': "pspace_distinct' s" and
           pspace_aligned': "pspace_aligned' s" and
                        al: "is_aligned ptr bits"
  shows "valid_untyped' d ptr bits idx s =
         (\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow>
                 obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow>
                 obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and>
                 obj_range' p ko \<inter>
                   usableUntypedRange (UntypedCap d ptr bits idx) = {})" apply (simp add: valid_untyped'_def) apply (simp add: ko_wp_at'_def) apply (rule arg_cong[where f=All]) apply (rule ext) apply (rule arg_cong[where f=All]) apply (rule ext) apply (case_tac "ksPSpace s ptr' = Some ko", simp_all) apply (frule pspace_alignedD'[OF _ pspace_aligned']) apply (frule pspace_distinctD'[OF _ pspace_distinct']) apply simp apply (frule aligned_ranges_subset_or_disjoint[OF al]) apply (fold obj_range'_def) apply (rule iffI) apply auto[1] apply (rule conjI) apply (rule ccontr, simp) apply (simp add: Set.psubset_eq) apply (erule conjE) apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp) apply (cut_tac is_aligned_no_overflow[OF al]) apply (auto simp add: obj_range'_def)[1] apply (clarsimp simp add: usableUntypedRange.simps Int_commute) apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp+) apply (cut_tac is_aligned_no_overflow[OF al]) apply (clarsimp simp add: obj_range'_def) apply (frule is_aligned_no_overflow) by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1
               nat_le_linear power_overflow sub_wrap add_0
               add_0_right word_add_increasing word_less_1 word_less_sub_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_untyped' d ptr bits idx s = (\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow> obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' p ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. (\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) \<noteq> {}) ptr' s) = (\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow> obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' p ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. (\<forall>ptr' ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow> obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' p ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>ptr'. \<forall>ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (\<lambda>p. \<forall>ko. ksPSpace s p = Some ko \<longrightarrow> obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' p ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr'. (\<forall>ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (\<forall>ko. ksPSpace s ptr' = Some ko \<longrightarrow> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr'. (\<lambda>ko. is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (\<lambda>ko. ksPSpace s ptr' = Some ko \<longrightarrow> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. (is_aligned ptr' (objBitsKO ko) \<longrightarrow> ksPSpace s ptr' = Some ko \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (ksPSpace s ptr' = Some ko \<longrightarrow> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. ksPSpace s ptr' = Some ko \<Longrightarrow> (is_aligned ptr' (objBitsKO ko) \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko)\<rbrakk> \<Longrightarrow> (is_aligned ptr' (objBitsKO ko) \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (is_aligned ptr' (objBitsKO ko) \<longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} \<or> \<not> ps_clear ptr' (objBitsKO ko) s) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<or> {ptr'..ptr' + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> (\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> (\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) = (obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}) proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}; {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}; {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<and> {ptr..ptr + 2 ^ bits - 1} \<noteq> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}; {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko; {ptr..ptr + 2 ^ bits - 1} \<noteq> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}; {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko; {ptr..ptr + 2 ^ bits - 1} \<noteq> obj_range' ptr' ko; \<not> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (2 subgoals):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}; {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko; {ptr..ptr + 2 ^ bits - 1} \<noteq> obj_range' ptr' ko; \<not> obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}; ptr \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> obj_range' ptr' ko = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d ptr bits idx) = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> obj_range' ptr' ko \<or> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1}; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range' ptr' ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> obj_range' ptr' ko \<inter> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} = {}; idx < 2 ^ bits\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; idx < 2 ^ bits; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; idx < 2 ^ bits; obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} = {}; ptr \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; idx < 2 ^ bits; ptr \<le> ptr + 2 ^ bits - 1; ptr' \<le> ptr + 2 ^ bits - 1; ptr + word_of_nat idx \<le> ptr' + 2 ^ objBitsKO ko - 1; ptr + word_of_nat idx \<le> ptr + 2 ^ bits - 1; \<not> ptr \<le> ptr' + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' ko. \<lbrakk>ksPSpace s ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) s; idx < 2 ^ bits; ptr \<le> ptr + 2 ^ bits - 1; ptr' \<le> ptr + 2 ^ bits - 1; ptr + word_of_nat idx \<le> ptr' + 2 ^ objBitsKO ko - 1; ptr + word_of_nat idx \<le> ptr + 2 ^ bits - 1; \<not> ptr \<le> ptr' + 2 ^ objBitsKO ko - 1; ptr' \<le> ptr' + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> False