theory KHeap_R

lemma cte_wp_at_ctes_of:
  "cte_wp_at' P p s = (\<exists>cte. ctes_of s p = Some cte \<and> P cte)" apply (simp add: cte_wp_at_cases' map_to_ctes_def Let_def
                   cte_level_bits_def objBits_simps'
          split del: if_split) apply (safe del: disjCI) apply (clarsimp simp: ps_clear_def3 field_simps) apply (clarsimp simp: ps_clear_def3 field_simps
              split del: if_split) apply (frule is_aligned_sub_helper) apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) apply (case_tac "n = 0") apply (clarsimp simp: field_simps) apply (subgoal_tac "ksPSpace s p = None") apply clarsimp apply (clarsimp simp: field_simps) apply (elim conjE) apply (subst(asm) mask_in_range, assumption) apply (drule arg_cong[where f="\<lambda>S. p \<in> S"]) apply (simp add: dom_def field_simps) apply (erule mp) apply (rule ccontr, simp add: linorder_not_le) apply (drule word_le_minus_one_leq) apply clarsimp apply (simp add: field_simps) apply (clarsimp split: if_split_asm del: disjCI) apply (simp add: ps_clear_def3 field_simps) apply (rule disjI2, rule exI[where x="p - (p && ~~ mask 9)"]) apply (clarsimp simp: ps_clear_def3[where na=9] is_aligned_mask
                        word_bw_assocs field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p s = (\<exists>cte. ctes_of s p = Some cte \<and> P cte) proof (prove)
goal (1 subgoal):
 1. ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))) = (\<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte) proof (prove)
goal (3 subgoals):
 1. \<And>cte. \<lbrakk>ksPSpace s p = Some (KOCTE cte); is_aligned p 4; P cte; ps_clear p 4 s\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 3. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> n < 2 ^ 9
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 3. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n = 0\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 3. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0; ksPSpace s p = None\<rbrakk> \<Longrightarrow> \<exists>cte. (if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte \<and> P cte
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 3. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (3 subgoals):
 1. \<And>tcb getF setF. \<lbrakk>ksPSpace s (p - (p && mask 9)) = Some (KOTCB tcb); is_aligned (p - (p && mask 9)) 9; tcb_cte_cases (p && mask 9) = Some (getF, setF); P (getF tcb); {1 + p - (p && mask 9)..p + 0x1FF - (p && mask 9)} \<inter> dom (ksPSpace s) = {}; p && ~~ mask 9 = p - (p && mask 9); p && mask 9 \<noteq> 0; ksPSpace s p = None\<rbrakk> \<Longrightarrow> {1 + (p - (p && mask 9))..p - (p && mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {}
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 3. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; p && mask 9 = n \<and> p && ~~ mask 9 = p - n; n \<noteq> 0\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; n \<noteq> 0; p && mask 9 = n; p && ~~ mask 9 = p - n\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s) = {}; n \<noteq> 0; p && mask 9 = n; p \<in> {p - n..p - n + 2 ^ 9 - 1}\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); n \<noteq> 0; p && mask 9 = n; p \<in> {p - n..p - n + 2 ^ 9 - 1}; (p \<in> {1 + p - n..p + 0x1FF - n} \<inter> dom (ksPSpace s)) = (p \<in> {})\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); n \<noteq> 0; p && mask 9 = n; p - n \<le> p \<and> p \<le> p + 0x1FF - n; 1 + p - n \<le> p \<longrightarrow> ksPSpace s p = None\<rbrakk> \<Longrightarrow> ksPSpace s p = None
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); n \<noteq> 0; p && mask 9 = n; p - n \<le> p \<and> p \<le> p + 0x1FF - n\<rbrakk> \<Longrightarrow> 1 + p - n \<le> p
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); n \<noteq> 0; p && mask 9 = n; p - n \<le> p \<and> p \<le> p + 0x1FF - n; p < 1 + p - n\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); P (getF tcb); n \<noteq> 0; p && mask 9 = n; p - n \<le> p \<and> p \<le> p + 0x1FF - n; p \<le> 1 + p - n - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {p + 1..0xF + p} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {(p && ~~ mask 9) + 1..0x1FF + (p && ~~ mask 9)} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(if (\<exists>cte. ksPSpace s p = Some (KOCTE cte)) \<and> is_aligned p 4 \<and> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s p of Some (KOCTE x) \<Rightarrow> Some x else if (\<exists>tcb. ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb)) \<and> {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {} then case ksPSpace s (p && ~~ mask 9) of Some (KOTCB tcb) \<Rightarrow> map_option (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (p - (p && ~~ mask 9))) else None) = Some cte; P cte\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>P cte; is_aligned p 4; {1 + p..p + 0xF} \<inter> dom (ksPSpace s) = {}; ksPSpace s p = Some (KOCTE cte)\<rbrakk> \<Longrightarrow> ps_clear p 4 s \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s))
 2. \<And>tcb a b. \<lbrakk>P (a tcb); is_aligned p 4 \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) \<noteq> {}; {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb); tcb_cte_cases (p - (p && ~~ mask 9)) = Some (a, b)\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a b. \<lbrakk>P (a tcb); is_aligned p 4 \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) \<noteq> {}; {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb); tcb_cte_cases (p - (p && ~~ mask 9)) = Some (a, b)\<rbrakk> \<Longrightarrow> (\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> P cte \<and> ps_clear p 4 s) \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - n) 9 s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb a b. \<lbrakk>P (a tcb); is_aligned p 4 \<longrightarrow> (\<forall>cte. ksPSpace s p \<noteq> Some (KOCTE cte)) \<or> {1 + p..p + 0xF} \<inter> dom (ksPSpace s) \<noteq> {}; {1 + (p && ~~ mask 9)..(p && ~~ mask 9) + 0x1FF} \<inter> dom (ksPSpace s) = {}; ksPSpace s (p && ~~ mask 9) = Some (KOTCB tcb); tcb_cte_cases (p - (p && ~~ mask 9)) = Some (a, b)\<rbrakk> \<Longrightarrow> \<exists>tcb. ksPSpace s (p - (p - (p && ~~ mask 9))) = Some (KOTCB tcb) \<and> is_aligned (p - (p - (p && ~~ mask 9))) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases (p - (p && ~~ mask 9)) = Some (getF, setF)) \<and> P (getF tcb) \<and> ps_clear (p - (p - (p && ~~ mask 9))) 9 s) proof (prove)
goal:
No subgoals!