theory Tcb_R

lemma invokeTCB_corres:
 "tcbinv_relation ti ti' \<Longrightarrow>
  corres (dc \<oplus> (=))
         (einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti)
         (invs' and sch_act_simple and tcb_inv_wf' ti')
         (invoke_tcb ti) (invokeTCB ti')" apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def) apply (rule corres_guard_imp [OF invokeTCB_WriteRegisters_corres], simp+)[1] apply (rule corres_guard_imp [OF invokeTCB_ReadRegisters_corres], simp+)[1] apply (rule corres_guard_imp [OF invokeTCB_CopyRegisters_corres], simp+)[1] apply (clarsimp simp del: invoke_tcb.simps) apply (rename_tac word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11) apply (rule_tac F="is_aligned word 5" in corres_req) apply (clarsimp simp add: is_aligned_weaken [OF tcb_aligned]) apply (rule corres_guard_imp [OF transferCaps_corres], clarsimp+) apply (clarsimp simp: is_cnode_or_valid_arch_def
                      split: option.split option.split_asm) apply clarsimp apply (auto split: option.split_asm simp: newroot_rel_def)[1] apply (simp add: invokeTCB_def liftM_def[symmetric]
                      o_def dc_def[symmetric]) apply (rule corres_guard_imp [OF suspend_corres], simp+) apply (simp add: invokeTCB_def liftM_def[symmetric]
                     o_def dc_def[symmetric]) apply (rule corres_guard_imp [OF restart_corres], simp+) apply (simp add:invokeTCB_def) apply (rename_tac option) apply (case_tac option) apply simp apply (rule corres_guard_imp) apply (rule corres_split[OF unbindNotification_corres]) apply (rule corres_trivial, simp) apply wp+ apply (clarsimp) apply clarsimp apply simp apply (rule corres_guard_imp) apply (rule corres_split[OF bindNotification_corres]) apply (rule corres_trivial, simp) apply wp+ apply clarsimp apply (clarsimp simp: obj_at_def is_ntfn) apply (clarsimp simp: obj_at'_def projectKOs) apply (simp add: invokeTCB_def tlsBaseRegister_def) apply (rule corres_guard_imp) apply (rule corres_split[OF TcbAcc_R.asUser_setRegister_corres]) apply (rule corres_split[OF Bits_R.getCurThread_corres]) apply (rule corres_split[OF Corres_UL.corres_when]) apply simp apply (rule TcbAcc_R.rescheduleRequired_corres) apply (rule corres_trivial, simp) apply (wpsimp wp: hoare_drop_imp)+ apply (clarsimp simp: valid_sched_weak_strg einvs_valid_etcbs) apply (clarsimp simp: Tcb_R.invs_valid_queues' Invariants_H.invs_queues) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcbinv_relation ti ti' \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf ti) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb ti) (invokeTCB ti') proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>ti' = tcbinvocation.WriteRegisters x11 x12 x13 (copyregsets_map x14); ti = tcb_invocation.WriteRegisters x11 x12 x13 x14\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.WriteRegisters x11 x12 x13 x14)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.WriteRegisters x11 x12 x13 (copyregsets_map x14))) (invoke_tcb (tcb_invocation.WriteRegisters x11 x12 x13 x14)) (invokeTCB (tcbinvocation.WriteRegisters x11 x12 x13 (copyregsets_map x14)))
 2. \<And>x21 x22 x23 x24. \<lbrakk>ti' = tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24); ti = tcb_invocation.ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ReadRegisters x21 x22 x23 x24)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24))) (invoke_tcb (tcb_invocation.ReadRegisters x21 x22 x23 x24)) (invokeTCB (tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24)))
 3. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>ti' = tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37); ti = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37))) (invoke_tcb (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invokeTCB (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37)))
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>\<exists>flt_ep' croot' vroot' sl' buf'. x43 = map_option to_bl flt_ep' \<and> newroot_rel x46 croot' \<and> newroot_rel x47 vroot' \<and> ({x46, x47, map_option undefined x48} \<noteq> {None} \<longrightarrow> sl' = cte_map x42) \<and> (case x48 of None \<Rightarrow> buf' = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. buf' = Some (vptr, g''') \<and> newroot_rel g'' g''') \<and> ti' = tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'; ti = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invokeTCB ti')
 5. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 6. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 7. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 8. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>ti' = tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24); ti = tcb_invocation.ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ReadRegisters x21 x22 x23 x24)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24))) (invoke_tcb (tcb_invocation.ReadRegisters x21 x22 x23 x24)) (invokeTCB (tcbinvocation.ReadRegisters x21 x22 x23 (copyregsets_map x24)))
 2. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>ti' = tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37); ti = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37))) (invoke_tcb (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invokeTCB (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37)))
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>\<exists>flt_ep' croot' vroot' sl' buf'. x43 = map_option to_bl flt_ep' \<and> newroot_rel x46 croot' \<and> newroot_rel x47 vroot' \<and> ({x46, x47, map_option undefined x48} \<noteq> {None} \<longrightarrow> sl' = cte_map x42) \<and> (case x48 of None \<Rightarrow> buf' = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. buf' = Some (vptr, g''') \<and> newroot_rel g'' g''') \<and> ti' = tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'; ti = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invokeTCB ti')
 4. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 5. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 6. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 7. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>ti' = tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37); ti = tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37))) (invoke_tcb (tcb_invocation.CopyRegisters x31 x32 x33 x34 x35 x36 x37)) (invokeTCB (tcbinvocation.CopyRegisters x31 x32 x33 x34 x35 x36 (copyregsets_map x37)))
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>\<exists>flt_ep' croot' vroot' sl' buf'. x43 = map_option to_bl flt_ep' \<and> newroot_rel x46 croot' \<and> newroot_rel x47 vroot' \<and> ({x46, x47, map_option undefined x48} \<noteq> {None} \<longrightarrow> sl' = cte_map x42) \<and> (case x48 of None \<Rightarrow> buf' = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. buf' = Some (vptr, g''') \<and> newroot_rel g'' g''') \<and> ti' = tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'; ti = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invokeTCB ti')
 3. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 4. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 5. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>\<exists>flt_ep' croot' vroot' sl' buf'. x43 = map_option to_bl flt_ep' \<and> newroot_rel x46 croot' \<and> newroot_rel x47 vroot' \<and> ({x46, x47, map_option undefined x48} \<noteq> {None} \<longrightarrow> sl' = cte_map x42) \<and> (case x48 of None \<Rightarrow> buf' = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. buf' = Some (vptr, g''') \<and> newroot_rel g'' g''') \<and> ti' = tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'; ti = tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb (tcb_invocation.ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)) (invokeTCB ti')
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>x41 a b x44 x45 x46 x47 x48 flt_ep' croot' vroot' sl' buf'. \<lbrakk>ti = tcb_invocation.ThreadControl x41 (a, b) (map_option to_bl flt_ep') x44 x45 x46 x47 x48; newroot_rel x46 croot'; newroot_rel x47 vroot'; (\<exists>a aa b. x46 = Some (a, aa, b)) \<longrightarrow> sl' = cte_map (a, b); (\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> sl' = cte_map (a, b); (\<exists>a b. x48 = Some (a, b)) \<longrightarrow> sl' = cte_map (a, b); case x48 of None \<Rightarrow> buf' = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. buf' = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x41 and (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case x46 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case x46 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case x47 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case x47 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case x48 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case x48 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case x48 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. x46 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s) \<and> ((\<exists>a aa b. x47 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s) \<and> ((\<exists>a b. x48 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (a, b) s)) and (\<lambda>y. case flt_ep' of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32) and (\<lambda>s. case x45 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case x44 of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and ex_nonz_cap_to x41)) (invs' and sch_act_simple and (tcb_at' x41 and ex_nonz_cap_to' x41 and (\<lambda>y. valid_option_prio x45 \<and> valid_option_prio x44) and (case croot' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case croot' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case vroot' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case vroot' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case buf' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case buf' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case buf' of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case buf' of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. croot' = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) sl' s) \<and> ((\<exists>a b. vroot' = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) sl' s) \<and> ((\<exists>a b. buf' = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) sl' s)) and (\<lambda>s. case x45 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case x44 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) (invoke_tcb (tcb_invocation.ThreadControl x41 (a, b) (map_option to_bl flt_ep') x44 x45 x46 x47 x48)) (invokeTCB (tcbinvocation.ThreadControl x41 sl' flt_ep' x44 x45 croot' vroot' buf'))
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at word and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case t4 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t5 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a b. t6 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s)) and (\<lambda>y. case t7 of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and ex_nonz_cap_to word)) (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) (invoke_tcb (tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6)) (invokeTCB (tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11))
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (6 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11 s s'. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; (s, s') \<in> state_relation; (einvs and simple_sched_action and (tcb_at word and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case t4 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t5 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a b. t6 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s)) and (\<lambda>y. case t7 of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and ex_nonz_cap_to word)) s; (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) s'\<rbrakk> \<Longrightarrow> is_aligned word 5
 2. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at word and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case t4 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t5 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a b. t6 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s)) and (\<lambda>y. case t7 of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and ex_nonz_cap_to word)) (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) (invoke_tcb (tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6)) (invokeTCB (tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11))
 3. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 4. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 5. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at word and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (\<lambda>y. case t4 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t5 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t6 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2)) and (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) and (\<lambda>s. ((\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s) \<and> ((\<exists>a b. t6 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s)) and (\<lambda>y. case t7 of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s) and ex_nonz_cap_to word)) (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) (invoke_tcb (tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6)) (invokeTCB (tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11))
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (6 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11 s. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5; invs s; valid_list s; valid_sched s; simple_sched_action s; tcb_at word s; (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; case t4 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_cnode_cap (fst x2); (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s; (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; case t5 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_valid_vtable_root (fst x2); (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s; (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap (fst x2)) s; (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> no_cap_to_obj_dr_emp (fst x2)) s; case t6 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; case t6 of None \<Rightarrow> True | Some v \<Rightarrow> case snd v of None \<Rightarrow> True | Some x2 \<Rightarrow> valid_ipc_buffer_cap (fst x2) (fst v) \<and> is_arch_cap (fst x2) \<and> is_cnode_or_valid_arch (fst x2); (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2) and ex_cte_cap_wp_to (\<lambda>_. True) (snd x2)) s; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s; (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s; (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> cte_wp_at (\<lambda>_. True) (one, t2) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (one, t2) s; case t7 of None \<Rightarrow> True | Some x2 \<Rightarrow> word_bits = 32; case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) pr) auth s; case mcp of None \<Rightarrow> True | Some (mcp, auth) \<Rightarrow> mcpriority_tcb_at ((\<le>) mcp) auth s; ex_nonz_cap_to word s\<rbrakk> \<Longrightarrow> (case t4 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) s \<and> (case t5 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) s \<and> (case t6 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at (\<lambda>_. True) (snd x2)) s
 2. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11 s. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5; (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and (\<lambda>s. {t8, t9, map_option undefined t11} \<noteq> {None} \<longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (one, t2)) s) and K (case t8 of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case t9 of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and K (case t11 of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>v. is_aligned v msg_align_bits) \<circ> fst) x) and K (case t11 of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (valid_cap' \<circ> fst) \<circ> snd) x) and tcb_at' word and ex_nonz_cap_to' word and K (valid_option_prio t3 \<and> valid_option_prio mcp) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)) s
 3. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 4. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 5. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11 s. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5; (invs' and sch_act_simple and (tcb_at' word and ex_nonz_cap_to' word and (\<lambda>y. valid_option_prio t3 \<and> valid_option_prio mcp) and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) and (\<lambda>y. case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) and (\<lambda>s. ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s)) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s))) s\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple and (case t8 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and (\<lambda>s. {t8, t9, map_option undefined t11} \<noteq> {None} \<longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (one, t2)) s) and K (case t8 of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case t9 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case t9 of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and K (case t11 of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>v. is_aligned v msg_align_bits) \<circ> fst) x) and K (case t11 of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x) and (case t11 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (case_option (\<lambda>_. True) (valid_cap' \<circ> fst) \<circ> snd) x) and tcb_at' word and ex_nonz_cap_to' word and K (valid_option_prio t3 \<and> valid_option_prio mcp) and (\<lambda>s. case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) and (\<lambda>s. case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)) s
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>word one t2 mcp t3 t4 t5 t6 t7 t8 t9 t10 t11 s. \<lbrakk>ti = tcb_invocation.ThreadControl word (one, t2) (map_option to_bl t7) mcp t3 t4 t5 t6; newroot_rel t4 t8; newroot_rel t5 t9; (\<exists>a aa b. t4 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a aa b. t5 = Some (a, aa, b)) \<longrightarrow> t10 = cte_map (one, t2); (\<exists>a b. t6 = Some (a, b)) \<longrightarrow> t10 = cte_map (one, t2); case t6 of None \<Rightarrow> t11 = None | Some (vptr, g'') \<Rightarrow> \<exists>g'''. t11 = Some (vptr, g''') \<and> newroot_rel g'' g'''; ti' = tcbinvocation.ThreadControl word t10 t7 mcp t3 t8 t9 t11; is_aligned word 5; invs' s; sch_act_simple s; tcb_at' word s; ex_nonz_cap_to' word s; valid_option_prio t3; valid_option_prio mcp; (case t8 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case t8 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2); (case t9 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case t9 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2); (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; (case t11 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s; case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; case t11 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); (\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s; (\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s; (\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) t10 s; case t3 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s; case mcp of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s\<rbrakk> \<Longrightarrow> ((\<exists>a b. t8 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (one, t2)) s) \<and> ((\<exists>a b. t9 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (one, t2)) s) \<and> ((\<exists>a b. t11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (one, t2)) s)
 2. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 3. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 4. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (4 subgoals):
 1. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Suspend x5)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Suspend x5)) (invoke_tcb (tcb_invocation.Suspend x5)) (invokeTCB (tcbinvocation.Suspend x5))
 2. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 3. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 4. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (4 subgoals):
 1. \<And>x5. \<lbrakk>ti' = tcbinvocation.Suspend x5; ti = tcb_invocation.Suspend x5\<rbrakk> \<Longrightarrow> corres dc (einvs and simple_sched_action and (tcb_at x5 and ex_nonz_cap_to x5)) (invs' and sch_act_simple and (tcb_at' x5 and ex_nonz_cap_to' x5)) (IpcCancel_A.suspend x5) (ThreadDecls_H.suspend x5)
 2. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.Resume x6)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.Resume x6)) (invoke_tcb (tcb_invocation.Resume x6)) (invokeTCB (tcbinvocation.Resume x6))
 3. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 4. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x6 and ex_nonz_cap_to x6)) (invs' and sch_act_simple and (tcb_at' x6 and ex_nonz_cap_to' x6)) (liftE (do y <- Tcb_A.restart x6;
return []
od)) (invokeTCB (tcbinvocation.Resume x6))
 2. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x6. \<lbrakk>ti' = tcbinvocation.Resume x6; ti = tcb_invocation.Resume x6\<rbrakk> \<Longrightarrow> corres dc (einvs and simple_sched_action and (tcb_at x6 and ex_nonz_cap_to x6)) (invs' and sch_act_simple and (tcb_at' x6 and ex_nonz_cap_to' x6)) (Tcb_A.restart x6) (ThreadDecls_H.restart x6)
 2. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.NotificationControl x71 x72)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.NotificationControl x71 x72)) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case x72 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case x72 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (invokeTCB (tcbinvocation.NotificationControl x71 x72))
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 x72; ti = tcb_invocation.NotificationControl x71 x72\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case x72 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case x72 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 x72)) (case x72 of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = None\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 2. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> corres (=) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71)) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) (do y <- unbind_notification x71;
return []
od) (do y <- unbindNotification x71;
return []
od)
 2. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> corres (=) (?Q3763 x71 option) (?Q'3763 x71 option) (do y <- unbind_notification x71;
return []
od) (do y <- unbindNotification x71;
return []
od)
 2. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71)) s\<rbrakk> \<Longrightarrow> ?Q3763 x71 option s
 3. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) s\<rbrakk> \<Longrightarrow> ?Q'3763 x71 option s
 4. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (7 subgoals):
 1. \<And>x71 option y ya. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R3767 x71 option y) (?R'3767 x71 option ya) (return []) (return [])
 2. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q3767 x71 option\<rbrace> unbind_notification x71 \<lbrace>?R3767 x71 option\<rbrace>
 3. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3767 x71 option\<rbrace> unbindNotification x71 \<lbrace>?R'3767 x71 option\<rbrace>
 4. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71)) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and ?Q3767 x71 option) s
 5. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ?Q'3767 x71 option) s
 6. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 7. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (6 subgoals):
 1. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q3767 x71 option\<rbrace> unbind_notification x71 \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>x71 option. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3767 x71 option\<rbrace> unbindNotification x71 \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71)) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and ?Q3767 x71 option) s
 4. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ?Q'3767 x71 option) s
 5. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (4 subgoals):
 1. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71)) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and (\<lambda>s. True)) s
 2. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and (\<lambda>s. True)) s
 3. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 4. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x71 option s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 None; ti = tcb_invocation.NotificationControl x71 None; option = None; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71)) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and (\<lambda>s. True)) s
 2. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 option; ti = tcb_invocation.NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x71))) (invoke_tcb (tcb_invocation.NotificationControl x71 option)) (case option of None \<Rightarrow> liftE (do y <- unbindNotification x71;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification x71 ntfnPtr;
return []
od))
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> corres (=) (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) (do y <- bind_notification x71 a;
return []
od) (do y <- bindNotification x71 a;
return []
od)
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (4 subgoals):
 1. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> corres (=) (?Q3780 x71 option a) (?Q'3780 x71 option a) (do y <- bind_notification x71 a;
return []
od) (do y <- bindNotification x71 a;
return []
od)
 2. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) s\<rbrakk> \<Longrightarrow> ?Q3780 x71 option a s
 3. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> ?Q'3780 x71 option a s
 4. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (6 subgoals):
 1. \<And>x71 option a y ya. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R3784 x71 option a y) (?R'3784 x71 option a ya) (return []) (return [])
 2. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q3784 x71 option a\<rbrace> bind_notification x71 a \<lbrace>?R3784 x71 option a\<rbrace>
 3. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3784 x71 option a\<rbrace> bindNotification x71 a \<lbrace>?R'3784 x71 option a\<rbrace>
 4. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and ntfn_at a and ?Q3784 x71 option a) s
 5. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ntfn_at' a and ?Q'3784 x71 option a) s
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (5 subgoals):
 1. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q3784 x71 option a\<rbrace> bind_notification x71 a \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>x71 option a. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3784 x71 option a\<rbrace> bindNotification x71 a \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and ntfn_at a and ?Q3784 x71 option a) s
 4. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ntfn_at' a and ?Q'3784 x71 option a) s
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (einvs and simple_sched_action and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs and tcb_at x71 and ntfn_at a and (\<lambda>s. True)) s
 2. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ntfn_at' a and (\<lambda>_. True)) s
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (3 subgoals):
 1. \<And>x71 a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); invs s; valid_list s; valid_sched s; simple_sched_action s; tcb_at x71 s; ex_nonz_cap_to x71 s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> Structures_A.ntfn.WaitingNtfn q)) a s; ex_nonz_cap_to a s; bound_tcb_at ((=) None) x71 s\<rbrakk> \<Longrightarrow> ntfn_at a s
 2. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ntfn_at' a and (\<lambda>_. True)) s
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a s. \<lbrakk>ti' = tcbinvocation.NotificationControl x71 (Some a); ti = tcb_invocation.NotificationControl x71 (Some a); option = Some a; (invs' and sch_act_simple and (tcb_at' x71 and ex_nonz_cap_to' x71 and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' x71 and ntfn_at' a and (\<lambda>_. True)) s
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (dc \<oplus> (=)) (einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.SetTLSBase x81 x82)) (invs' and sch_act_simple and tcb_inv_wf' (tcbinvocation.SetTLSBase x81 x82)) (invoke_tcb (tcb_invocation.SetTLSBase x81 x82)) (invokeTCB (tcbinvocation.SetTLSBase x81 x82)) proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (=) (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) (do y <- as_user x81 (setRegister MachineExports.tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) reschedule_required;
return []
od) (do y <- asUser x81 (setRegister MachineExports.tlsBaseRegister x82);
cur <- getCurThread;
y <- when (x81 = cur) rescheduleRequired;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> corres (=) (?Q3841 x81 x82) (?Q'3841 x81 x82) (do y <- as_user x81 (setRegister MachineExports.tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) reschedule_required;
return []
od) (do y <- asUser x81 (setRegister MachineExports.tlsBaseRegister x82);
cur <- getCurThread;
y <- when (x81 = cur) rescheduleRequired;
return []
od)
 2. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> ?Q3841 x81 x82 s
 3. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> ?Q'3841 x81 x82 s proof (prove)
goal (5 subgoals):
 1. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R3845 x81 x82 y) (?R'3845 x81 x82 ya) (do cur <- gets cur_thread;
y <- when (x81 = cur) reschedule_required;
return []
od) (do cur <- getCurThread;
y <- when (x81 = cur) rescheduleRequired;
return []
od)
 2. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>?R3845 x81 x82\<rbrace>
 3. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>?R'3845 x81 x82\<rbrace>
 4. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
 5. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and ?Q'3845 x81 x82) s proof (prove)
goal (7 subgoals):
 1. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> corres (=) (?R3850 x81 x82 y ya cur) (?R'3850 x81 x82 y ya cura) (do y <- when (x81 = cur) reschedule_required;
return []
od) (do y <- when (x81 = cura) rescheduleRequired;
return []
od)
 2. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q3851 x81 x82 y\<rbrace> gets cur_thread \<lbrace>?R3850 x81 x82 y ya\<rbrace>
 3. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3852 x81 x82 ya\<rbrace> getCurThread \<lbrace>?R'3850 x81 x82 y ya\<rbrace>
 4. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q3851 x81 x82 y\<rbrace>
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'3852 x81 x82 ya\<rbrace>
 6. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
 7. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and ?Q'3845 x81 x82) s proof (prove)
goal (11 subgoals):
 1. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> (x81 = cur) = (x81 = cura)
 2. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> corres dc (?P3859 x81 x82 y ya cur) (?P'3862 x81 x82 y ya cura) reschedule_required rescheduleRequired
 3. \<And>x81 x82 y ya cur cura yb yc. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R3856 x81 x82 y ya cur cura yb) (?R'3856 x81 x82 y ya cur cura yc) (return []) (return [])
 4. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q3860 x81 x82 y ya cur\<rbrace> when (x81 = cur) reschedule_required \<lbrace>?R3856 x81 x82 y ya cur cura\<rbrace>
 5. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3863 x81 x82 y ya cura\<rbrace> when (x81 = cura) rescheduleRequired \<lbrace>?R'3856 x81 x82 y ya cur cura\<rbrace>
 6. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q3851 x81 x82 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>x. x81 = cur \<longrightarrow> ?P3859 x81 x82 y ya cur x) and ?Q3860 x81 x82 y ya cur\<rbrace>
 7. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3852 x81 x82 ya\<rbrace> getCurThread \<lbrace>\<lambda>cura. (\<lambda>x. x81 = cura \<longrightarrow> ?P'3862 x81 x82 y ya cura x) and ?Q'3863 x81 x82 y ya cura\<rbrace>
 8. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q3851 x81 x82 y\<rbrace>
 9. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'3852 x81 x82 ya\<rbrace>
 10. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> corres dc (?P3859 x81 x82 y ya cur) (?P'3862 x81 x82 y ya cura) reschedule_required rescheduleRequired
 2. \<And>x81 x82 y ya cur cura yb yc. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R3856 x81 x82 y ya cur cura yb) (?R'3856 x81 x82 y ya cur cura yc) (return []) (return [])
 3. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q3860 x81 x82 y ya cur\<rbrace> when (x81 = cur) reschedule_required \<lbrace>?R3856 x81 x82 y ya cur cura\<rbrace>
 4. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3863 x81 x82 y ya cura\<rbrace> when (x81 = cura) rescheduleRequired \<lbrace>?R'3856 x81 x82 y ya cur cura\<rbrace>
 5. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q3851 x81 x82 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>x. x81 = cur \<longrightarrow> ?P3859 x81 x82 y ya cur x) and ?Q3860 x81 x82 y ya cur\<rbrace>
 6. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3852 x81 x82 ya\<rbrace> getCurThread \<lbrace>\<lambda>cura. (\<lambda>x. x81 = cura \<longrightarrow> ?P'3862 x81 x82 y ya cura x) and ?Q'3863 x81 x82 y ya cura\<rbrace>
 7. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q3851 x81 x82 y\<rbrace>
 8. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'3852 x81 x82 ya\<rbrace>
 9. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
 10. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and ?Q'3845 x81 x82) s proof (prove)
goal (9 subgoals):
 1. \<And>x81 x82 y ya cur cura yb yc. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R3856 x81 x82 y ya cur cura yb) (?R'3856 x81 x82 y ya cur cura yc) (return []) (return [])
 2. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q3860 x81 x82 y ya cur\<rbrace> when (x81 = cur) reschedule_required \<lbrace>?R3856 x81 x82 y ya cur cura\<rbrace>
 3. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3863 x81 x82 y ya cura\<rbrace> when (x81 = cura) rescheduleRequired \<lbrace>?R'3856 x81 x82 y ya cur cura\<rbrace>
 4. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q3851 x81 x82 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>x. x81 = cur \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and ?Q3860 x81 x82 y ya cur\<rbrace>
 5. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3852 x81 x82 ya\<rbrace> getCurThread \<lbrace>\<lambda>cura. (\<lambda>x. x81 = cura \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and ?Q'3863 x81 x82 y ya cura\<rbrace>
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q3851 x81 x82 y\<rbrace>
 7. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'3852 x81 x82 ya\<rbrace>
 8. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
 9. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and ?Q'3845 x81 x82) s proof (prove)
goal (8 subgoals):
 1. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q3860 x81 x82 y ya cur\<rbrace> when (x81 = cur) reschedule_required \<lbrace>\<lambda>yb _. True\<rbrace>
 2. \<And>x81 x82 y ya cur cura. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya; cur = cura\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3863 x81 x82 y ya cura\<rbrace> when (x81 = cura) rescheduleRequired \<lbrace>\<lambda>yc _. True\<rbrace>
 3. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q3851 x81 x82 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>x. x81 = cur \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and ?Q3860 x81 x82 y ya cur\<rbrace>
 4. \<And>x81 x82 y ya. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3852 x81 x82 ya\<rbrace> getCurThread \<lbrace>\<lambda>cura. (\<lambda>x. x81 = cura \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and ?Q'3863 x81 x82 y ya cura\<rbrace>
 5. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q3845 x81 x82\<rbrace> as_user x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q3851 x81 x82 y\<rbrace>
 6. \<And>x81 x82. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3845 x81 x82\<rbrace> asUser x81 (setRegister MachineExports.tlsBaseRegister x82) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'3852 x81 x82 ya\<rbrace>
 7. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (einvs and simple_sched_action and (tcb_at x81 and ex_nonz_cap_to x81)) s\<rbrakk> \<Longrightarrow> (tcb_at x81 and ?Q3845 x81 x82) s
 8. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and ?Q'3845 x81 x82) s proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; invs s; valid_list s; valid_sched s; simple_sched_action s; tcb_at x81 s; ex_nonz_cap_to x81 s\<rbrakk> \<Longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s
 2. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and (\<lambda>s. True \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82 s. \<lbrakk>ti' = tcbinvocation.SetTLSBase x81 x82; ti = tcb_invocation.SetTLSBase x81 x82; (invs' and sch_act_simple and (tcb_at' x81 and ex_nonz_cap_to' x81)) s\<rbrakk> \<Longrightarrow> (tcb_at' x81 and (\<lambda>s. True \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s proof (prove)
goal:
No subgoals!