theory Tcb_C

lemma getObject_context:
  " \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk>
  \<Longrightarrow> (if t = t' then tcbContext_update (\<lambda>_. st) x else x,
      s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)
      \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))" apply (simp split: if_split) apply (rule conjI) apply clarsimp apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad
                         Corres_C.in_magnitude_check' projectKOs objBits_simps') apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs objBits_simps) apply (simp add: magnitudeCheck_def in_monad split: option.splits) apply clarsimp apply (simp add: lookupAround2_char2) apply (clarsimp split: if_split_asm) apply (erule_tac x=x2 in allE) apply (clarsimp simp: ps_clear_def) apply (drule_tac x=x2 in orthD2) apply fastforce apply clarsimp apply (erule impE) apply simp apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) apply simp apply clarsimp apply (clarsimp simp: getObject_def split_def loadObject_default_def in_monad
                        Corres_C.in_magnitude_check' projectKOs objBits_simps') apply (simp add: magnitudeCheck_def in_monad split: option.splits) apply clarsimp apply (simp add: lookupAround2_char2) apply (clarsimp split: if_split_asm) apply (erule_tac x=t in allE) apply simp apply (clarsimp simp: obj_at'_real_def projectKOs
                         ko_wp_at'_def objBits_simps) apply (simp add: ps_clear_def) apply (drule_tac x=t in orthD2) apply fastforce apply clarsimp apply (erule impE) apply 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 (clarsimp simp: 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 fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> (if t = t' then tcbContext_update (\<lambda>_. st) x else x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> (t = t' \<longrightarrow> (tcbContext_update (\<lambda>_. st) x, s'\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))) \<and> (t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t = t' \<longrightarrow> (tcbContext_update (\<lambda>_. st) x, s'\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t' s; t = t'\<rbrakk> \<Longrightarrow> (tcbContext_update (\<lambda>_. st) x, s'\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' ko t' s; t = t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s\<rbrakk> \<Longrightarrow> tcbContext_update (\<lambda>_. st) ko = tcbContext_update (\<lambda>_. st) x \<and> ((), s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t' < 0x200
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s; snd (lookupAround2 t' ((ksPSpace s)(t' \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko)))) = Some x2; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s; t' < x2 \<and> (\<exists>y. (if x2 = t' then Some (KOTCB (tcbContext_update (\<lambda>_. st) ko)) else ksPSpace s x2) = Some y) \<and> (\<forall>z. t' < z \<and> z < x2 \<longrightarrow> (if z = t' then Some (KOTCB (tcbContext_update (\<lambda>_. st) ko)) else ksPSpace s z) = None); x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s; 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\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ps_clear t' 9 s; is_aligned t' tcbBlockSizeBits; x = ko; ps_clear t' tcbBlockSizeBits s; t' < x2; ksPSpace s x2 = Some y; (t' < x2 \<longrightarrow> x2 \<noteq> t') \<and> (x2 < x2 \<longrightarrow> t' < x2 \<longrightarrow> x2 = t' \<or> ksPSpace s x2 = None)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; ({t'..0x1FF + t'} - {t'}) \<inter> dom (ksPSpace s) = {}; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s)
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; t' \<le> x2 \<longrightarrow> \<not> x2 \<le> 0x1FF + t'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> t' \<le> x2
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; \<not> x2 \<le> 0x1FF + t'\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; \<not> x2 \<le> 0x1FF + t'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> x2 - t' \<le> 0x1FF
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 3. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); is_aligned t' 9; s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; t = t'; ksPSpace s t' = Some (KOTCB ko); s' = s; is_aligned t' tcbBlockSizeBits; x = ko; ({t'..t' + 2 ^ tcbBlockSizeBits - 1} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < x2; ksPSpace s x2 = Some y; x2 \<noteq> t'; t' \<le> t' + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s\<rbrakk> \<Longrightarrow> t \<noteq> t' \<longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, s') \<in> fst (getObject t' s); ko_at' ko t s; t \<noteq> t'\<rbrakk> \<Longrightarrow> (x, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (getObject t' (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (magnitudeCheck t' (snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))))) 9 (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s\<rbrakk> \<Longrightarrow> \<forall>x2. snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko)))) = Some x2 \<longrightarrow> \<not> x2 - t' < 0x200 proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; snd (lookupAround2 t' ((ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko)))) = Some x2; x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; t' < x2 \<and> (\<exists>y. (if x2 = t then Some (KOTCB (tcbContext_update (\<lambda>_. st) ko)) else ksPSpace s x2) = Some y) \<and> (\<forall>z. t' < z \<and> z < x2 \<longrightarrow> (if z = t then Some (KOTCB (tcbContext_update (\<lambda>_. st) ko)) else ksPSpace s z) = None); x2 - t' < 0x200\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; t' < t; \<forall>z<t. t' < z \<longrightarrow> z = t \<or> ksPSpace s z = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; t' < t; t < t \<longrightarrow> t' < t \<longrightarrow> t = t \<or> ksPSpace s t = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; t' < t\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; t' < t; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ({t'..0x1FF + t'} - {t'}) \<inter> dom (ksPSpace s) = {}; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; ksPSpace s t = Some (KOTCB ko); is_aligned t tcbBlockSizeBits; ({t..t + 2 ^ tcbBlockSizeBits - 1} - {t}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> t' \<le> t
 2. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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
 3. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t - t' < 0x200; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); s' = s; t' < t; 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>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; 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\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ps_clear t' 9 s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; (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 proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; ({t'..0x1FF + t'} - {t'}) \<inter> dom (ksPSpace s) = {}; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<in> dom (ksPSpace s)
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 \<notin> {t'..0x1FF + t'} - {t'}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; x2 \<le> 0x1FF + t' \<longrightarrow> t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 \<le> 0x1FF + t'
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> x2 - t' \<le> 0x1FF
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 3. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> t' + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> t' \<le> 0x1FF + t'
 2. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 y. \<lbrakk>x2 - t' < 0x200; ko_at' ko t s; t \<noteq> t'; ksPSpace s t' = Some (KOTCB x); is_aligned t' 9; s' = s; x2 \<noteq> t; t' < x2; ksPSpace s x2 = Some y; t' \<le> x2 \<longrightarrow> x2 = t'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!