theory Tcb_C

lemma asUser_state:
  "\<lbrakk>(x,s) \<in> fst (asUser t' f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> \<rbrakk> \<Longrightarrow>
  (x,s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in>
  fst (asUser t' f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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 (1) threadGet_state) 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_state) apply (intro exI) apply (erule conjI) apply (clarsimp simp: setObject_def split_def updateObject_default_def threadGet_def
                        in_magnitude_check' getObject_def loadObject_default_def liftM_def
                        objBits_simps' projectKOs in_monad) apply (simp split: if_split) apply (rule conjI) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) apply (rule conjI) apply clarsimp apply (cases s, simp) apply (rule ext) apply (clarsimp split: if_split) apply (cases ko) apply clarsimp apply clarsimp apply (rule conjI) apply (clarsimp simp add: lookupAround2_char2 split: if_split_asm) 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, simp) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) apply simp apply (rule exI) apply (rule conjI, fastforce) apply clarsimp apply (cases s, clarsimp) apply (rule ext, clarsimp split: if_split) apply (cases ko, clarsimp) apply (clarsimp simp: magnitudeCheck_def in_monad split: option.splits) apply (rule conjI) apply clarsimp apply (cases s, clarsimp) apply (rule ext, clarsimp split: if_split) apply (case_tac tcb, clarsimp) 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 t' f s); ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (x, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (asUser t' f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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>; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s'')\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' 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>; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' 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>; (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f uc); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s''); s = s''; uc = b\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s)\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s); (b, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st23 b) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st23 b) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>b. (x, b) \<in> fst (f uc) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s); (b, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st23 b) ko))\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st23 b) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?uc27 b, ?s''26 b) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> (\<exists>ba. (x, ba) \<in> fst (f (?uc27 b)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet ba (tcbArch tcb)) tcb) t' (?s''26 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (x, b) \<in> fst (f b); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s)\<rbrakk> \<Longrightarrow> \<exists>ba. (x, ba) \<in> fst (f b) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet ba (tcbArch tcb)) tcb) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); ((), s) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s'')\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s'') \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s''); s = s''\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s) \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s)\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s) \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s); (if t = t' then tcbState_update (\<lambda>_. ?st57 b tcb) tcb else tcb, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st57 b tcb) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st57 b tcb) ko))\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s) \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s); (if t = t' then tcbState_update (\<lambda>_. ?st57 b tcb) tcb else tcb, s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st57 b tcb) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. ?st57 b tcb) ko))\<rparr>))\<rbrakk> \<Longrightarrow> (?tcb61 b tcb, ?s''60 b tcb) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch (?tcb61 b tcb))) (?tcb61 b tcb)) (?s''60 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>; (b, s) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t' s); (tcb, s) \<in> fst (getObject t' s); ((), s) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) s)\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (setObject t' (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch (if t = t' then tcbState_update (\<lambda>_. st) tcb else tcb))) (if t = t' then tcbState_update (\<lambda>_. st) tcb else tcb)) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<exists>b. (if t' = t then Some (KOTCB (tcbState_update (\<lambda>_. st) ko)) else ksPSpace s t') = Some b \<and> (\<exists>uu_. b = KOTCB uu_) \<and> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch tcb)) (tcbArch (if t = t' then tcbState_update (\<lambda>_. st) tcb else tcb))) (if t = t' then tcbState_update (\<lambda>_. st) tcb else 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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> (t' = t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t (snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) (tcbState_update (\<lambda>_. st) tcb)))\<rparr>)) \<and> (t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' = t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t (snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) (tcbState_update (\<lambda>_. st) tcb)))\<rparr>)
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<exists>s''. ((), s'') \<in> fst (magnitudeCheck t (snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> (snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>) \<and> (\<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>))
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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 (tcbState_update (\<lambda>_. st) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState x. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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 (tcbState_update (\<lambda>_. st) ko))) x = (ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))) x
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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> tcbState_update (\<lambda>_. st) ko = tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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>; ko = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> tcbState_update (\<lambda>_. st) ko = tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<not> x2 - t < 0x200 \<and> (\<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>)
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<not> x2 - t < 0x200
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; t < x2; \<forall>z. (t < z \<longrightarrow> z \<noteq> t) \<and> (z < x2 \<longrightarrow> t < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; (t < x2 \<longrightarrow> x2 \<noteq> t) \<and> (x2 < x2 \<longrightarrow> t < x2 \<longrightarrow> x2 = t \<or> ksPSpace s x2 = None)\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ({t..0x1FF + t} - {t}) \<inter> dom (ksPSpace s) = {}; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s)
 2. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t; x2 \<notin> {t..0x1FF + t} - {t}\<rbrakk> \<Longrightarrow> False
 3. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 4. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t; x2 \<notin> {t..0x1FF + t} - {t}\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t; t \<le> x2 \<longrightarrow> \<not> x2 \<le> 0x1FF + t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t; \<not> x2 \<le> 0x1FF + t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> x2 - t \<le> 0x1FF
 2. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> t \<le> 0x1FF + t
 3. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 4. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t\<rbrakk> \<Longrightarrow> t \<le> 0x1FF + t
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' = t; t < x2; ksPSpace s x2 = Some y; x2 - t < 0x200; x2 \<noteq> t; t \<le> t + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> t \<le> 0x1FF + t
 2. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 3. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> (\<not> x2 - t < 0x200 \<longrightarrow> ?s''258 x2 = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = ?s''258 x2\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)), ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr>; is_aligned t 9; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t' = t; snd (lookupAround2 t ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))\<rparr>
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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 (tcbState_update (\<lambda>_. st) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)))
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ps_clear t 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(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko)); is_aligned t 9; ksPSpace t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits \<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>; t' = t; snd (lookupAround2 t (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) 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> tcbState_update (\<lambda>_. st) ko = tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko)
 2. \<And>tcb. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> t' \<noteq> t \<longrightarrow> (\<exists>s''. ((), s'') \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None \<longrightarrow> t' \<noteq> t \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>) \<and> (\<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None \<longrightarrow> t' \<noteq> t \<longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None; t' \<noteq> t\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace t' = Some (KOTCB tcb); ps_clear t' 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(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned t' 9; snd (lookupAround2 t' (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None; t' \<noteq> t; 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 (tcbState_update (\<lambda>_. st) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace t' = Some (KOTCB tcb); ps_clear t' 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(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned t' 9; snd (lookupAround2 t' (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = None; t' \<noteq> t; 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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> t' \<noteq> t \<longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<not> x2 - t' < 0x200 \<and> (\<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<not> x2 - t' < 0x200
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; \<forall>z<t. t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None; t - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; \<forall>z<t. t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None; t - t' < 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>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; t < t \<longrightarrow> t' < t \<longrightarrow> t = t \<or> ksPSpace s t = None\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 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>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ({t'..0x1FF + t'} - {t'}) \<inter> dom (ksPSpace s) = {}; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 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>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 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>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' \<le> t \<longrightarrow> \<not> t \<le> 0x1FF + t'\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 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 + t'\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t - t' \<le> 0x1FF
 2. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 3. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>t' \<noteq> t; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; t' < t; t - t' < 0x200; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}; t' \<le> t' + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; \<forall>z. (t' < z \<longrightarrow> z = t \<longrightarrow> \<not> t < x2) \<and> (z < x2 \<longrightarrow> t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None); ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; (t' < x2 \<longrightarrow> x2 = t \<longrightarrow> \<not> t < x2) \<and> (x2 < x2 \<longrightarrow> t' < 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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ({t'..0x1FF + t'} - {t'}) \<inter> dom (ksPSpace s) = {}; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s)
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; x2 \<le> 0x1FF + t' \<longrightarrow> t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> x2 \<le> 0x1FF + t'
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> x2 - t' \<le> 0x1FF
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 3. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 4. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> t' + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 3. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x2 y. \<lbrakk>t' \<noteq> t; ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 - t' < 0x200; x2 = t'\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb x2. \<lbrakk>ko_at' ko t s; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> \<exists>s''. (\<not> x2 - t' < 0x200 \<longrightarrow> s'' = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> (\<not> x2 - t' < 0x200 \<longrightarrow> ?s''593 tcb x2 = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<and> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = ?s''593 tcb x2\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)), ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace s t' = Some (KOTCB tcb); ps_clear t' 9 s; s = s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb))\<rparr>; is_aligned t' 9; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t\<rbrakk> \<Longrightarrow> s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace t' = Some (KOTCB tcb); ps_clear t' 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(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned t' 9; snd (lookupAround2 t' (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t; 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 (tcbState_update (\<lambda>_. st) ko)) = ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko), t' \<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>; ksPSpace t' = Some (KOTCB tcb); ps_clear t' 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(t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch tcb) tcb)); is_aligned t' 9; snd (lookupAround2 t' (ksPSpace(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)))) = Some x2; t' \<noteq> t; 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!