theory Detype_R

lemma cte_map_untyped_range:
  "\<lbrakk> s \<turnstile> cap; cte_at cref s; pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> (cte_map cref \<in> untyped_range cap) = (fst cref \<in> untyped_range cap)" apply (cases cap, simp_all) apply (drule(2) cte_map_obj_range_helper) apply (clarsimp simp: valid_cap_def valid_untyped_def) apply (elim allE, drule(1) mp) apply (rule iffI) apply (erule impE) apply (rule notemptyI[where x="cte_map cref"]) apply simp apply clarsimp apply (drule subsetD [OF _ p_in_obj_range]) apply simp+ apply (erule impE) apply (rule notemptyI[where x="fst cref"]) apply (simp add: p_in_obj_range) apply clarsimp apply (drule(1) subsetD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; cte_wp_at (\<lambda>_. True) cref s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> (cte_map cref \<in> untyped_range cap) = (fst cref \<in> untyped_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap.UntypedCap x21 x22 x23 x24; cte_wp_at (\<lambda>_. True) cref s; pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1) = (x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap.UntypedCap x21 x22 x23 x24; pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; \<exists>ko. kheap s (fst cref) = Some ko \<and> cte_map cref \<in> obj_range (fst cref) ko\<rbrakk> \<Longrightarrow> (x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1) = (x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> (x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1) = (x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> (x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1) = (x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 3. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> cte_map cref \<in> obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1}
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 3. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref; cte_map cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref; cte_map cref \<le> x22 + 2 ^ x23 - 1; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> kheap (?s29 x21 x22 x23 x24 ko) (fst cref) = Some ko
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref; cte_map cref \<le> x22 + 2 ^ x23 - 1; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> pspace_aligned (?s29 x21 x22 x23 x24 ko)
 3. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref; cte_map cref \<le> x22 + 2 ^ x23 - 1; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> valid_objs (?s29 x21 x22 x23 x24 ko)
 4. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> cte_map cref; cte_map cref \<le> x22 + 2 ^ x23 - 1; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; fst cref \<in> {x22..x22 + 2 ^ x23 - 1}\<rbrakk> \<Longrightarrow> x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1
 5. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1\<rbrakk> \<Longrightarrow> fst cref \<in> obj_range (fst cref) ko \<inter> {x22..x22 + 2 ^ x23 - 1}
 2. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref \<and> fst cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref; fst cref \<le> x22 + 2 ^ x23 - 1; obj_range (fst cref) ko \<subseteq> {x22..x22 + 2 ^ x23 - 1}; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 ko. \<lbrakk>pspace_aligned s; valid_objs s; cap = cap.UntypedCap x21 x22 x23 x24; cap_aligned (cap.UntypedCap x21 x22 x23 x24); kheap s (fst cref) = Some ko; cte_map cref \<in> obj_range (fst cref) ko; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; x22 \<le> fst cref; fst cref \<le> x22 + 2 ^ x23 - 1; (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range (fst cref) ko = {}; cte_map cref \<in> {x22..x22 + 2 ^ x23 - 1}\<rbrakk> \<Longrightarrow> x22 \<le> cte_map cref \<and> cte_map cref \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal:
No subgoals!