theory Tcb_C

lemma asUser_context:
  "\<lbrakk>(x,s) \<in> fst (asUser (ksCurThread s) f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> ;
    t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow>
  (x,s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in>
  fst (asUser (ksCurThread s) f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>))" apply (clarsimp simp: asUser_def in_monad select_f_def) apply (frule use_valid, rule threadGet_inv [where P="(=) s"], rule refl) apply (frule use_valid, assumption, rule refl) apply clarsimp apply (frule (2) threadGet_context) apply (intro exI) apply (erule conjI) apply (rule exI, erule conjI) apply (clarsimp simp: threadSet_def in_monad) apply (frule use_valid, rule getObject_inv [where P="(=) s"]) apply (simp add: loadObject_default_def) apply wp apply simp apply (rule refl) apply clarsimp apply (frule (1) getObject_context) apply (intro exI) apply (erule conjI) apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def
                        Corres_C.in_magnitude_check' getObject_def loadObject_default_def liftM_def
                        objBits_simps' projectKOs in_monad) apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) apply (rule conjI) apply clarsimp apply (cases s, simp) apply (rule ext, clarsimp split: if_split) apply (case_tac tcb, simp) apply clarsimp apply (rule conjI) apply (clarsimp simp add: lookupAround2_char2 split: if_split_asm) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) apply (erule_tac x=t in allE) apply simp apply (simp add: ps_clear_def) apply (drule_tac x=t in orthD2) apply fastforce apply clarsimp apply (erule impE, simp) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) apply simp apply (erule_tac x=x2 in allE) apply simp apply (simp add: ps_clear_def) apply (drule_tac x=x2 in orthD2) apply fastforce apply clarsimp apply (erule impE) apply (rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) apply simp apply (erule impE, simp) apply simp apply (rule exI) apply (rule conjI, fastforce) apply clarsimp apply (cases s, clarsimp) apply (rule ext, clarsimp split: if_split) apply (case_tac tcb, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, s) \<in> fst (asUser (ksCurThread s) f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> (x, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (asUser (ksCurThread s) f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s''); s = s''; uc = b\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s)\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s); (b, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st23 b) (tcbArch ko)) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st23 b) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s'')) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s); (b, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st23 b) (tcbArch ko)) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (?st23 b) (tcbArch ko)) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?uc28 b, ?s''27 b) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> (\<exists>ba. (x, ba) \<in> fst (f (?uc28 b)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet ba (tcbArch tcb)) tcb) (ksCurThread s) (?s''27 b))) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s)\<rbrakk> \<Longrightarrow> \<exists>ba. (x, ba) \<in> fst (f b) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet ba (tcbArch tcb)) tcb) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (3 subgoals):
 1. \<And>b s'' tcb p q n koa. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> loadObject p q n koa \<lbrace>\<lambda>rv. (=) s\<rbrace>
 2. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> s = s
 3. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (3 subgoals):
 1. \<And>b s'' tcb p q n koa. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- assert (p = q);
val <- projectKO koa;
y <- alignCheck p (objBits val);
y <- magnitudeCheck p n (objBits val);
return val
od \<lbrace>\<lambda>rv. (=) s\<rbrace>
 2. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> s = s
 3. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (3 subgoals):
 1. \<And>b s'' tcb p q n koa sa. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = sa\<rbrakk> \<Longrightarrow> p = q \<longrightarrow> s = sa
 2. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> s = s
 3. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (2 subgoals):
 1. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> s = s
 2. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>b s'' tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s'') \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>b tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s) \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s)\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>b tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s) \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s); (if t = ksCurThread s then ?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) tcb else tcb, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>b tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s) \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s); (if t = ksCurThread s then ?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) tcb else tcb, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) ko))\<rparr>) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (?tcbContext_update58 b tcb (\<lambda>_. ?st58 b tcb) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?tcb62 b tcb, ?s''61 b tcb) \<in> fst (getObject (ksCurThread s) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch (?tcb62 b tcb))) (?tcb62 b tcb)) (?s''61 b tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>b tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) (ksCurThread s) s); (tcb, s) \<in> fst (getObject (ksCurThread s) s); ((), s) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject (ksCurThread s) (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch (if t = ksCurThread s then tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko else tcb))) (if t = ksCurThread s then tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko else tcb)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<exists>s''. ((), s'') \<in> fst (magnitudeCheck (ksCurThread s) (snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> (snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = None \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) \<and> (\<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = None \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = None\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_at' ko t \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread; ksPSpace ksCurThread = Some (KOTCB tcb); ps_clear ksCurThread 9 \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace = ksPSpace(ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned ksCurThread 9; snd (lookupAround2 ksCurThread (ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = None; s = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>tcb ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_at' ko t \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread; ksPSpace ksCurThread = Some (KOTCB tcb); ps_clear ksCurThread 9 \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace = ksPSpace(ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned ksCurThread 9; snd (lookupAround2 ksCurThread (ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = None; s = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> tcb = tcbArch_update (\<lambda>_. tcbArch tcb) tcb
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2 \<longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<not> x2 - ksCurThread s < 0x200 \<and> (\<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<not> x2 - ksCurThread s < 0x200
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; \<forall>z<t. ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None; t - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; \<forall>z<t. ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t < t \<longrightarrow> ksCurThread s < t \<longrightarrow> t = t \<or> ksPSpace s t = None\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ({ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}) \<inter> dom (ksPSpace s) = {}; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t \<in> dom (ksPSpace s)
 2. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t \<notin> {ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t \<notin> {ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; ksCurThread s \<le> t \<longrightarrow> \<not> t \<le> 0x1FF + ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; \<not> t \<le> 0x1FF + ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t - ksCurThread s \<le> 0x1FF
 2. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 3. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; ksCurThread s < t; t - ksCurThread s < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; ksCurThread s \<le> ksCurThread s + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; \<forall>z. (ksCurThread s < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> ksCurThread s < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; (ksCurThread s < x2 \<longrightarrow> x2 = t \<longrightarrow> \<not> t < x2) \<and> (x2 < x2 \<longrightarrow> ksCurThread s < x2 \<longrightarrow> x2 = t \<or> ksPSpace s x2 = None)\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ({ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}) \<inter> dom (ksPSpace s) = {}; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s)
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; x2 \<notin> {ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; x2 \<notin> {ksCurThread s..0x1FF + ksCurThread s} - {ksCurThread s}\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; x2 \<le> 0x1FF + ksCurThread s \<longrightarrow> ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> x2 \<le> 0x1FF + ksCurThread s
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> x2 - ksCurThread s \<le> 0x1FF
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 3. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> ksCurThread s + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> ksCurThread s \<le> 0x1FF + ksCurThread s
 2. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; ksCurThread s \<le> x2 \<longrightarrow> x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; x2 \<noteq> t; ksCurThread s < x2; ksPSpace s x2 = Some y; x2 - ksCurThread s < 0x200; x2 = ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> (\<not> x2 - ksCurThread s < 0x200 \<longrightarrow> ?s''376 tcb x2 = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = ?s''376 tcb x2\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)), ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread s; ksPSpace s (ksCurThread s) = Some (KOTCB tcb); ps_clear (ksCurThread s) 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned (ksCurThread s) 9; snd (lookupAround2 (ksCurThread s) ((ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread s \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2 ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_at' ko t \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread; ksPSpace ksCurThread = Some (KOTCB tcb); ps_clear ksCurThread 9 \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace = ksPSpace(ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned ksCurThread 9; snd (lookupAround2 ksCurThread (ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2; s = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko), ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2 ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>ko_at' ko t \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; t \<noteq> ksCurThread; ksPSpace ksCurThread = Some (KOTCB tcb); ps_clear ksCurThread 9 \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; ksPSpace = ksPSpace(ksCurThread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned ksCurThread 9; snd (lookupAround2 ksCurThread (ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet st (tcbArch ko)) ko)))) = Some x2; s = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> tcb = tcbArch_update (\<lambda>_. tcbArch tcb) tcb proof (prove)
goal:
No subgoals!