theory Detype_R

lemma locateCTE_monad:
  assumes ko_wp_at: "\<And>Q dest.
  \<lbrace>\<lambda>s. P1 s \<and> ko_wp_at' (\<lambda>obj. Q (objBitsKO obj))  dest s \<rbrace> f
  \<lbrace>\<lambda>a s. ko_wp_at' (\<lambda>obj. Q (objBitsKO obj)) dest s\<rbrace>"
  assumes cte_wp_at: "\<And> dest.
  \<lbrace>\<lambda>s. P2 s \<and> cte_wp_at' \<top> dest s \<rbrace> f
  \<lbrace>\<lambda>a s. cte_wp_at' \<top> dest s\<rbrace>"
  assumes psp_distinct:
  "\<lbrace>\<lambda>s. P3 s \<rbrace> f \<lbrace>\<lambda>a s. pspace_distinct' s\<rbrace>"
  assumes psp_aligned:
  "\<lbrace>\<lambda>s. P4 s \<rbrace> f \<lbrace>\<lambda>a s. pspace_aligned' s\<rbrace>"
  shows
  "\<lbrakk>{(ptr, s)} = fst (locateCTE src s);
    (r, s') \<in> fst (f s);pspace_aligned' s;pspace_distinct' s;(P1 and P2 and P3 and P4) s\<rbrakk>
   \<Longrightarrow> {(ptr,s')} = fst (locateCTE src s')" proof - have src_in_range:
   "\<And>obj src a m s'. \<lbrakk>cte_check obj src a m;ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1}" proof - fix obj src a m show "\<And>s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1}" by (case_tac obj)
         (auto simp add: cte_check_def objBits_simps' diff_eq_eq
                         add.commute[where b=a]
                         word_plus_mono_right is_aligned_no_wrap'
                         tcbVTableSlot_def tcbCTableSlot_def tcbReplySlot_def
                         tcbCallerSlot_def tcbIPCBufferSlot_def ) qed note blah[simp del] = usableUntypedRange.simps atLeastAtMost_iff
          atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have step1:
    "\<lbrakk>(ptr, s) \<in> fst (locateCTE src s);
      (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk>
     \<Longrightarrow> (ptr,s') \<in> fst (locateCTE src s')" apply (frule use_valid[OF _ locateCTE_case]) apply simp apply (clarsimp simp: locateCTE_def gets_def split_def
                        get_def bind_def return_def assert_opt_def fail_def assert_def
                  split: option.splits if_split_asm) apply (frule_tac dest1 = src in use_valid[OF _ cte_wp_at]) apply simp apply (subst cte_wp_at_top) apply simp apply (clarsimp simp add:cte_wp_at_top) apply (clarsimp simp:lookupAround2_char1) apply (frule_tac dest1 = ptr and  Q1 = "\<lambda>x. x = objBitsKO b" in use_valid[OF _ ko_wp_at]) apply (frule(1) pspace_alignedD') apply (frule(1) pspace_distinctD') apply (auto simp add:ko_wp_at'_def)[1] apply (clarsimp simp add:ko_wp_at'_def) apply (rule ccontr) apply (frule use_valid[OF _ psp_distinct]) apply simp apply (frule use_valid[OF _ psp_aligned]) apply simp apply (frule_tac x = a in pspace_distinctD') apply simp apply (frule_tac s = s' and a = ptr in rule_out_intv[rotated]) apply simp+ apply (frule_tac s = s' and b = ptr and a = a in rule_out_intv) apply simp+ apply (thin_tac "\<forall>x. P x \<longrightarrow> Q x" for P Q)+ apply (drule_tac p = ptr and p' = a in aligned_ranges_subset_or_disjoint) apply (erule(1) pspace_alignedD') apply (drule(1) src_in_range)+ apply (drule base_member_set[OF pspace_alignedD']) apply simp apply (simp add:objBitsKO_bounded2[unfolded word_bits_def,simplified]) apply (drule base_member_set[OF pspace_alignedD']) apply simp apply (simp add:objBitsKO_bounded2[unfolded word_bits_def,simplified]) apply (clarsimp simp: field_simps) apply (elim disjE; fastforce simp: mask_def p_assoc_help) done assume
    "{(ptr, s)} = fst (locateCTE src s)"
    "(r, s') \<in> fst (f s)"
    "pspace_aligned' s"
    "pspace_distinct' s"
    "(P1 and P2 and P3 and P4) s" thus ?thesis using assms step1 by (clarsimp simp:singleton_locateCTE) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (state)
goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (prove)
goal (1 subgoal):
 1. \<And>obj src a m s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1} proof (state)
goal (1 subgoal):
 1. \<And>obj src a m s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1} proof (state)
goal (1 subgoal):
 1. \<And>obj src a m s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cte_check obj src a m; ksPSpace s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1} proof (state)
this:
\<lbrakk>cte_check obj src a m; ksPSpace ?s' a = Some obj\<rbrakk> \<Longrightarrow> src \<in> {a..a + 2 ^ objBitsKO obj - 1}

goal:
No subgoals! proof (state)
this:
\<lbrakk>cte_check ?obj ?src ?a ?m; ksPSpace ?s' ?a = Some ?obj\<rbrakk> \<Longrightarrow> ?src \<in> {?a..?a + 2 ^ objBitsKO ?obj - 1}

goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (state)
this:
usableUntypedRange (capability.UntypedCap ?d ?p ?n ?f) = (if ?f < 2 ^ ?n then {?p + word_of_nat ?f..?p + 2 ^ ?n - 1} else {})
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> (ptr, s') \<in> fst (locateCTE src s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> True
 2. \<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s; \<exists>obj. ksPSpace s ptr = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> (ptr, s') \<in> fst (locateCTE src s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s; \<exists>obj. ksPSpace s ptr = Some obj \<and> (case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> (ptr, s') \<in> fst (locateCTE src s') proof (prove)
goal (1 subgoal):
 1. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> (\<exists>y. fst (lookupAround2 src (ksPSpace s')) = Some y) \<and> (\<forall>a b. fst (lookupAround2 src (ksPSpace s')) = Some (a, b) \<longrightarrow> (cte_check b src a (snd (lookupAround2 src (ksPSpace s'))) \<longrightarrow> ptr = a) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s')))) proof (prove)
goal (2 subgoals):
 1. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> P2 s \<and> cte_wp_at' (\<lambda>_. True) src s
 2. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_wp_at' (\<lambda>_. True) src s'\<rbrakk> \<Longrightarrow> (\<exists>y. fst (lookupAround2 src (ksPSpace s')) = Some y) \<and> (\<forall>a b. fst (lookupAround2 src (ksPSpace s')) = Some (a, b) \<longrightarrow> (cte_check b src a (snd (lookupAround2 src (ksPSpace s'))) \<longrightarrow> ptr = a) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s')))) proof (prove)
goal (2 subgoals):
 1. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s
 2. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_wp_at' (\<lambda>_. True) src s'\<rbrakk> \<Longrightarrow> (\<exists>y. fst (lookupAround2 src (ksPSpace s')) = Some y) \<and> (\<forall>a b. fst (lookupAround2 src (ksPSpace s')) = Some (a, b) \<longrightarrow> (cte_check b src a (snd (lookupAround2 src (ksPSpace s'))) \<longrightarrow> ptr = a) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s')))) proof (prove)
goal (2 subgoals):
 1. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s)))\<rbrakk> \<Longrightarrow> \<exists>a b. fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s)))
 2. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_wp_at' (\<lambda>_. True) src s'\<rbrakk> \<Longrightarrow> (\<exists>y. fst (lookupAround2 src (ksPSpace s')) = Some y) \<and> (\<forall>a b. fst (lookupAround2 src (ksPSpace s')) = Some (a, b) \<longrightarrow> (cte_check b src a (snd (lookupAround2 src (ksPSpace s'))) \<longrightarrow> ptr = a) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s')))) proof (prove)
goal (1 subgoal):
 1. \<And>b obj. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_wp_at' (\<lambda>_. True) src s'\<rbrakk> \<Longrightarrow> (\<exists>y. fst (lookupAround2 src (ksPSpace s')) = Some y) \<and> (\<forall>a b. fst (lookupAround2 src (ksPSpace s')) = Some (a, b) \<longrightarrow> (cte_check b src a (snd (lookupAround2 src (ksPSpace s'))) \<longrightarrow> ptr = a) \<and> cte_check b src a (snd (lookupAround2 src (ksPSpace s')))) proof (prove)
goal (1 subgoal):
 1. \<And>b obj a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; fst (lookupAround2 src (ksPSpace s)) = Some (ptr, b); ksPSpace s ptr = Some obj; case obj of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); fst (lookupAround2 src (ksPSpace s')) = Some (a, ba); cte_check ba src a (snd (lookupAround2 src (ksPSpace s')))\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None\<rbrakk> \<Longrightarrow> P1 s \<and> ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s
 2. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s'\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; is_aligned ptr (objBitsKO b)\<rbrakk> \<Longrightarrow> P1 s \<and> ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s
 2. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s'\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; is_aligned ptr (objBitsKO b); ps_clear ptr (objBitsKO b) s\<rbrakk> \<Longrightarrow> P1 s \<and> ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s
 2. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s'\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ko_wp_at' (\<lambda>obj. objBitsKO obj = objBitsKO b) ptr s'\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'\<rbrakk> \<Longrightarrow> ptr = a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a\<rbrakk> \<Longrightarrow> P3 s
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'\<rbrakk> \<Longrightarrow> P4 s
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'\<rbrakk> \<Longrightarrow> ptr \<noteq> a
 3. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'\<rbrakk> \<Longrightarrow> ksPSpace s' ptr = Some (?obj118 b a ba ko)
 4. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO (?obj118 b a ba ko))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b)\<rbrakk> \<Longrightarrow> ksPSpace s' ptr = Some (?obj'121 b a ba ko)
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b)\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 3. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b)\<rbrakk> \<Longrightarrow> a \<noteq> ptr
 4. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; \<forall>z. ptr < z \<and> z \<le> src \<longrightarrow> ksPSpace s z = None; a \<le> src; ksPSpace s' a = Some ba; \<forall>z. a < z \<and> z \<le> src \<longrightarrow> ksPSpace s' z = None; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; is_aligned ptr (objBitsKO b); objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba)\<rbrakk> \<Longrightarrow> is_aligned a (?n'134 b a ba ko)
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ ?n'134 b a ba ko - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ ?n'134 b a ba ko - 1} \<or> {a..a + 2 ^ ?n'134 b a ba ko - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; cte_check b src ptr (snd (lookupAround2 src (ksPSpace s))); cte_check ba src a (snd (lookupAround2 src (ksPSpace s'))); ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; ksPSpace s ptr = Some b; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}\<rbrakk> \<Longrightarrow> objBitsKO b < LENGTH(32)
 3. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}\<rbrakk> \<Longrightarrow> objBitsKO b < LENGTH(32)
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' a = Some ba; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> objBitsKO ba < LENGTH(32)
 3. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}; a \<in> {a..a + (2 ^ objBitsKO ba - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}\<rbrakk> \<Longrightarrow> objBitsKO ba < LENGTH(32)
 2. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}; a \<in> {a..a + (2 ^ objBitsKO ba - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + (2 ^ objBitsKO b - 1)}; a \<in> {a..a + (2 ^ objBitsKO ba - 1)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b a ba ko. \<lbrakk>(r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; P1 s; P2 s; P3 s; P4 s; case b of KOTCB tcb \<Rightarrow> True | KOCTE v \<Rightarrow> True | _ \<Rightarrow> False; ptr \<le> src; a \<le> src; ksPSpace s' ptr = Some ko; objBitsKO ko = objBitsKO b; ps_clear ptr (objBitsKO b) s'; ptr \<noteq> a; pspace_distinct' s'; pspace_aligned' s'; ps_clear a (objBitsKO ba) s'; a \<notin> mask_range ptr (objBitsKO b); ptr \<notin> mask_range a (objBitsKO ba); {ptr..ptr + 2 ^ objBitsKO b - 1} \<inter> {a..a + 2 ^ objBitsKO ba - 1} = {} \<or> {ptr..ptr + 2 ^ objBitsKO b - 1} \<subseteq> {a..a + 2 ^ objBitsKO ba - 1} \<or> {a..a + 2 ^ objBitsKO ba - 1} \<subseteq> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; src \<in> {a..a + 2 ^ objBitsKO ba - 1}; ptr \<in> {ptr..ptr + 2 ^ objBitsKO b - 1}; a \<in> {a..a + 2 ^ objBitsKO ba - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> (ptr, s') \<in> fst (locateCTE src s')

goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (state)
this:
{(ptr, s)} = fst (locateCTE src s)
(r, s') \<in> fst (f s)
pspace_aligned' s
pspace_distinct' s
(P1 and P2 and P3 and P4) s

goal (1 subgoal):
 1. \<lbrakk>{(ptr, s)} = fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> {(ptr, s')} = fst (locateCTE src s') proof (prove)
using this:
{(ptr, s)} = fst (locateCTE src s)
(r, s') \<in> fst (f s)
pspace_aligned' s
pspace_distinct' s
(P1 and P2 and P3 and P4) s

goal (1 subgoal):
 1. {(ptr, s')} = fst (locateCTE src s') proof (prove)
using this:
{(ptr, s)} = fst (locateCTE src s)
(r, s') \<in> fst (f s)
pspace_aligned' s
pspace_distinct' s
(P1 and P2 and P3 and P4) s
\<lbrace>\<lambda>s. P1 s \<and> ko_wp_at' (\<lambda>obj. ?Q (objBitsKO obj)) ?dest s\<rbrace> f \<lbrace>\<lambda>a. ko_wp_at' (\<lambda>obj. ?Q (objBitsKO obj)) ?dest\<rbrace>
\<lbrace>\<lambda>s. P2 s \<and> cte_wp_at' (\<lambda>_. True) ?dest s\<rbrace> f \<lbrace>\<lambda>a. cte_wp_at' (\<lambda>_. True) ?dest\<rbrace>
\<lbrace>P3\<rbrace> f \<lbrace>\<lambda>a. pspace_distinct'\<rbrace>
\<lbrace>P4\<rbrace> f \<lbrace>\<lambda>a. pspace_aligned'\<rbrace>
\<lbrakk>(ptr, s) \<in> fst (locateCTE src s); (r, s') \<in> fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\<rbrakk> \<Longrightarrow> (ptr, s') \<in> fst (locateCTE src s')

goal (1 subgoal):
 1. {(ptr, s')} = fst (locateCTE src s') proof (state)
this:
{(ptr, s')} = fst (locateCTE src s')

goal:
No subgoals!