theory Invariants_H

lemma typ_at_lift_valid_untyped':
  assumes P: "\<And>T p. \<lbrace>\<lambda>s. \<not>typ_at' T p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not>typ_at' T p s\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_untyped' d p n idx s\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' d p n idx s\<rbrace>" apply (clarsimp simp: valid_untyped'_def split del:if_split) apply (rule hoare_vcg_all_lift) apply (clarsimp simp: valid_def split del:if_split) apply (frule ko_wp_typ_at') apply clarsimp apply (cut_tac T=T and p=ptr' in P) apply (simp add: valid_def) apply (erule_tac x=s in allE) apply (erule impE) prefer 2 apply (drule (1) bspec) apply simp apply (clarsimp simp: typ_at'_def ko_wp_at'_def simp del:atLeastAtMost_iff) apply (elim disjE) apply (clarsimp simp:psubset_eq simp del:atLeastAtMost_iff) apply (drule_tac p=ptr' in koType_obj_range') apply (erule impE) apply simp apply simp apply (drule_tac p = ptr' in koType_obj_range') apply (clarsimp split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_untyped' d p n idx\<rbrace> f \<lbrace>\<lambda>rv. valid_untyped' d p n idx\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr'. \<lbrace>\<lambda>s. \<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; \<exists>T. typ_at' T ptr' b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; \<lbrace>\<lambda>s. \<not> typ_at' T ptr' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at' T ptr' s\<rbrace>\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; \<forall>s. \<not> typ_at' T ptr' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<not> typ_at' T ptr' s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; \<not> typ_at' T ptr' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<not> typ_at' T ptr' s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b\<rbrakk> \<Longrightarrow> \<not> typ_at' T ptr' s
 2. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; \<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<not> typ_at' T ptr' s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; \<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<not> typ_at' T ptr' s'\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b\<rbrakk> \<Longrightarrow> \<not> typ_at' T ptr' s proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b; case (a, b) of (r, s') \<Rightarrow> \<not> typ_at' T ptr' s'\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b\<rbrakk> \<Longrightarrow> \<not> typ_at' T ptr' s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b T. \<lbrakk>\<not> ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' s; (a, b) \<in> fst (f s); ko_wp_at' (\<lambda>ko. {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}) ptr' b; typ_at' T ptr' b\<rbrakk> \<Longrightarrow> \<not> typ_at' T ptr' s proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}; ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b ko kob x. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' kob \<longrightarrow> {p..p + 2 ^ n - 1} = obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' ko; x \<in> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> x \<in> {p..p + 2 ^ n - 1}
 2. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b ko kob x. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' kob \<longrightarrow> {p..p + 2 ^ n - 1} = obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' ko; x \<in> obj_range' ptr' ko; obj_range' ptr' kob = obj_range' ptr' ko\<rbrakk> \<Longrightarrow> x \<in> {p..p + 2 ^ n - 1}
 2. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>ptr' s a b ko kob x. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' ko; x \<in> obj_range' ptr' ko; obj_range' ptr' kob = obj_range' ptr' ko\<rbrakk> \<Longrightarrow> {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' kob
 2. \<And>ptr' s a b ko kob x. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' ko; x \<in> obj_range' ptr' ko; obj_range' ptr' kob = obj_range' ptr' ko; {p..p + 2 ^ n - 1} = obj_range' ptr' kob\<rbrakk> \<Longrightarrow> x \<in> {p..p + 2 ^ n - 1}
 3. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr' s a b ko kob x. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; {p..p + 2 ^ n - 1} \<subseteq> obj_range' ptr' ko; x \<in> obj_range' ptr' ko; obj_range' ptr' kob = obj_range' ptr' ko; {p..p + 2 ^ n - 1} = obj_range' ptr' kob\<rbrakk> \<Longrightarrow> x \<in> {p..p + 2 ^ n - 1}
 2. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; koTypeOf kob = koTypeOf ko; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr' s a b ko kob. \<lbrakk>(a, b) \<in> fst (f s); ksPSpace b ptr' = Some ko; is_aligned ptr' (objBitsKO ko); ps_clear ptr' (objBitsKO ko) b; is_aligned ptr' (objBitsKO kob); ksPSpace s ptr' = Some kob; ps_clear ptr' (objBitsKO kob) s; \<not> {p..p + 2 ^ n - 1} \<subset> obj_range' ptr' kob; obj_range' ptr' kob \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) = {}; obj_range' ptr' ko \<inter> (if idx < 2 ^ n then {p + word_of_nat idx..p + 2 ^ n - 1} else {}) \<noteq> {}; obj_range' ptr' kob = obj_range' ptr' ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!