theory Detype_R

lemma valid_untyped_no_overlap:
  "\<lbrakk> valid_untyped' d ptr bits idx s; is_aligned ptr bits; valid_pspace' s \<rbrakk>
  \<Longrightarrow> pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s |` (- {ptr .. ptr + 2 ^ bits - 1})\<rparr>)" apply (clarsimp simp del: atLeastAtMost_iff
            simp: pspace_no_overlap'_def valid_cap'_def valid_untyped'_def is_aligned_neg_mask_eq) apply (drule_tac x=x in spec) apply (drule restrict_map_Some_iff[THEN iffD1]) apply clarsimp apply (frule pspace_alignedD') apply (simp add: valid_pspace'_def) apply (frule pspace_distinctD') apply (simp add: valid_pspace'_def) apply (unfold ko_wp_at'_def obj_range'_def) apply (drule (1) aligned_ranges_subset_or_disjoint) apply (clarsimp simp del: Int_atLeastAtMost atLeastAtMost_iff atLeastatMost_subset_iff) apply (elim disjE) apply (subgoal_tac "ptr \<in> {x..x + 2 ^ objBitsKO ko - 1}") apply (clarsimp simp:p_assoc_help) apply (clarsimp simp:p_assoc_help) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_untyped' d ptr bits idx s; is_aligned ptr bits; valid_pspace' s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) ptr' s; is_aligned ptr bits; valid_pspace' s; (ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})) x = Some ko; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; (ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})) x = Some ko; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko \<and> x \<in> - {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko)\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko \<or> obj_range' x ko \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) x s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>is_aligned ptr bits; valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<nexists>ko. ksPSpace s x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> ({ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1} \<or> {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) \<and> ps_clear x (objBitsKO ko) s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); \<nexists>ko. ksPSpace s x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> ({ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1} \<or> {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) \<noteq> {}) \<and> ps_clear x (objBitsKO ko) s; ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {} \<or> {ptr..ptr + 2 ^ bits - 1} \<subseteq> {x..x + 2 ^ objBitsKO ko - 1} \<or> {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {} \<or> ptr = x \<and> ptr + 2 ^ bits = x + 2 ^ objBitsKO ko \<or> {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; ptr = x \<and> ptr + 2 ^ bits = x + 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> False
 3. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {}; ptr \<in> {x..x + 2 ^ objBitsKO ko - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {}\<rbrakk> \<Longrightarrow> ptr \<in> {x..x + 2 ^ objBitsKO ko - 1}
 3. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; ptr = x \<and> ptr + 2 ^ bits = x + 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> False
 4. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {ptr..ptr + 2 ^ bits - 1} \<inter> {x..x + 2 ^ objBitsKO ko - 1} = {}\<rbrakk> \<Longrightarrow> ptr \<in> {x..x + 2 ^ objBitsKO ko - 1}
 2. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; ptr = x \<and> ptr + 2 ^ bits = x + 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> False
 3. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; ptr = x \<and> ptr + 2 ^ bits = x + 2 ^ objBitsKO ko\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<lbrakk>valid_pspace' s; x \<le> ptr + (2 ^ bits - 1); ptr \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; ptr \<le> ptr + (2 ^ bits - 1); ksPSpace s x = Some ko; ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ bits - 1; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) s; \<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBitsKO ko - 1}; {x..x + 2 ^ objBitsKO ko - 1} \<inter> (if idx < 2 ^ bits then {ptr + word_of_nat idx..ptr + 2 ^ bits - 1} else {}) = {}; {x..x + 2 ^ objBitsKO ko - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!