theory Tcb_DR

lemma invoke_tcb_corres_copy_regs:
  "\<lbrakk> t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e;
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top>
   (invs and tcb_at obj_id' and tcb_at target_id' and Tcb_AI.tcb_inv_wf t' and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs)
     (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def arch_post_modify_registers_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule corres_cases [where R="a"]) apply (clarsimp simp: when_def) apply (rule corres_alternate1) apply (rule suspend_corres) apply (clarsimp simp: when_def dc_def[symmetric])+ apply (rule corres_alternate2) apply (rule corres_free_return [where P="\<top>" and P'="\<top>"]) apply (rule corres_split[where r'=dc]) apply (rule corres_cases [where R="b"]) apply (clarsimp simp: when_def) apply (rule corres_alternate1) apply (rule restart_corres, simp) apply (rule corres_alternate2) apply (rule corres_free_return [where P="\<top>" and P'="\<top>"]) apply (rule corres_corrupt_tcb_intent_dupl) apply (rule corres_split[where r'=dc]) apply (rule corres_cases [where R="c"]) apply (clarsimp simp: when_def) apply (rule corres_bind_ignore_ret_rhs) apply (rule corres_corrupt_tcb_intent_dupl) apply (rule corres_split[where r'=dc]) apply (rule invoke_tcb_corres_copy_regs_loop, simp) apply (rule corres_symb_exec_r) apply (simp add:setNextPC_def) apply (rule Intent_DR.set_register_corres[unfolded dc_def], simp) apply (wp | clarsimp simp:getRestartPC_def)+ apply (wp mapM_x_wp [where S=UNIV]) apply simp apply simp apply (rule dummy_corrupt_tcb_intent_corres) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'=dc]) apply (rule corres_cases [where R="d"]) apply (clarsimp simp: when_def) apply (rule invoke_tcb_corres_copy_regs_loop) apply (clarsimp simp: when_def) apply (rule dummy_corrupt_tcb_intent_corres) apply (rule corres_symb_exec_r) apply (rule corres_split_noop_rhs[OF corres_trivial]) apply simp apply (clarsimp simp: when_def) apply (rule reschedule_required_dcorres[THEN corres_trivial]) apply wpsimp+ apply (wp mapM_x_wp [where S=UNIV])[1] apply simp apply (wp wp_post_taut) apply (clarsimp simp:conj_comms pred_conj_def cong: if_cong) apply (wpsimp simp: not_idle_thread_def | rule conjI | strengthen invs_cur)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and tcb_at obj_id' and tcb_at target_id' and tcb_inv_wf t' and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) (do y <- Tcb_D.suspend target_id' \<sqinter> return ();
y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when a (IpcCancel_A.suspend target_id');
y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> dcorres dc ?Q1 ?Q'1 (do y <- Tcb_D.suspend target_id' \<sqinter> return ();
y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when a (IpcCancel_A.suspend target_id');
y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> dcorres dc ?P5 ?P'5 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; a\<rbrakk> \<Longrightarrow> dcorres dc ?P10 ?P'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> (?P10 and ?Q10 and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10 and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' True b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' True b c d 0; a\<rbrakk> \<Longrightarrow> dcorres dc ?P10 ?P'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (IpcCancel_A.suspend target_id')
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> (?P10 and ?Q10 and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10 and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' True b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' True b c d 0; a\<rbrakk> \<Longrightarrow> dcorres dc ?P10 ?P'10 (Tcb_D.suspend target_id') (IpcCancel_A.suspend target_id')
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> (?P10 and ?Q10 and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10 and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (when a (IpcCancel_A.suspend target_id'))
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 and ?Q5) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and ?Q'10 and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' False b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' False b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (Tcb_D.suspend target_id' \<sqinter> return ()) (return ())
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 and ?Q5) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and ?Q'10 and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' False b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' False b c d 0; \<not> a\<rbrakk> \<Longrightarrow> dcorres dc ?Q10 ?Q'10 (return ()) (return ())
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 and ?Q5) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and ?Q'10 and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R5 y) (?R'5 ya) (do y <- Tcb_D.restart obj_id' \<sqinter> return ();
corrupt_tcb_intent obj_id'
od) (do y <- when b (Tcb_A.restart obj_id');
y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>?R5\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?P24 y) (?P'26 ya) (Tcb_D.restart obj_id' \<sqinter> return ()) (when b (Tcb_A.restart obj_id'))
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. ?P24 y and ?Q25 y\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. ?P'26 ya and ?Q'27 ya\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; b\<rbrakk> \<Longrightarrow> dcorres dc (?P33 y) (?P'35 ya) (Tcb_D.restart obj_id' \<sqinter> return ()) (when b (Tcb_A.restart obj_id'))
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 y) (?Q'36 ya) (Tcb_D.restart obj_id' \<sqinter> return ()) (when b (Tcb_A.restart obj_id'))
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. ?P33 y and ?Q34 y and ?Q25 y\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. ?P'35 ya and ?Q'36 ya and ?Q'27 ya\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a True c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a True c d 0; b\<rbrakk> \<Longrightarrow> dcorres dc (?P33 ()) (?P'35 ()) (Tcb_D.restart obj_id' \<sqinter> return ()) (Tcb_A.restart obj_id')
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 y) (?Q'36 ya) (Tcb_D.restart obj_id' \<sqinter> return ()) (when b (Tcb_A.restart obj_id'))
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. ?P33 y and ?Q34 y and ?Q25 y\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. ?P'35 ya and ?Q'36 ya and ?Q'27 ya\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a True c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a True c d 0; b\<rbrakk> \<Longrightarrow> dcorres dc (?P33 ()) (?P'35 ()) (Tcb_D.restart obj_id') (Tcb_A.restart obj_id')
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 y) (?Q'36 ya) (Tcb_D.restart obj_id' \<sqinter> return ()) (when b (Tcb_A.restart obj_id'))
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. ?P33 y and ?Q34 y and ?Q25 y\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. ?P'35 ya and ?Q'36 ya and ?Q'27 ya\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a False c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a False c d 0; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 ()) (?Q'36 ()) (Tcb_D.restart obj_id' \<sqinter> return ()) (return ())
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q34 y and ?Q25 y\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and ?Q'36 ya and ?Q'27 ya\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a False c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a False c d 0; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc (?Q34 ()) (?Q'36 ()) (return ()) (return ())
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and ?Q34 y and ?Q25 y\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and ?Q'36 ya and ?Q'27 ya\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (corrupt_tcb_intent obj_id') (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?R23 y ya yb) (?R'23 y ya yc) (do corrupt_tcb_intent obj_id';
corrupt_tcb_intent obj_id'
od) (do y <- when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od);
y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>?R23 y ya\<rbrace>
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>?R'23 y ya\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (10 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> dcorres dc (?P50 y ya yb) (?P'52 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P50 y ya yb and ?Q51 y ya yb\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'52 y ya yc and ?Q'53 y ya yc\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (11 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; c\<rbrakk> \<Longrightarrow> dcorres dc (?P59 y ya yb) (?P'61 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P59 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'61 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres dc (?P59 () () ()) (?P'61 () () ()) (corrupt_tcb_intent obj_id') (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od)
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P59 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'61 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres dc (?P59 () () ()) (?P'61 () () ()) (corrupt_tcb_intent obj_id') (do mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od)
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P59 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'61 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres dc (?P59 () () ()) (?P'61 () () ()) (do corrupt_tcb_intent obj_id';
corrupt_tcb_intent obj_id'
od) (do mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od)
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P59 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'61 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres dc (?P87 () () ()) (?P'85 () () ()) (corrupt_tcb_intent obj_id') (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers)
 2. \<And>rv rv'. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R75 rv) (?R'75 rv') (K_bind (corrupt_tcb_intent obj_id') rv) (K_bind (do pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) rv')
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 () () ()\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R75\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>?R'75\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 6. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 8. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 9. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. ?P87 y ya yb and ?Q86 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 10. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. ?P'85 y ya yc and ?Q'84 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R75 ()) (?R'75 ()) (corrupt_tcb_intent obj_id') (do pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od)
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 () () ()\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R75\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>?R'75\<rbrace>
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 5. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and ?Q86 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 9. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and ?Q'84 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>pc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R75 ()) (?Q'93 pc) (corrupt_tcb_intent obj_id') (as_user obj_id' (setNextPC pc))
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?R'75 ()\<rbrace> as_user obj_id' getRestartPC \<lbrace>?Q'93\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; ?R'75 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> as_user obj_id' getRestartPC \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; False\<rbrakk> \<Longrightarrow> no_fail (?R'75 ()) (as_user obj_id' getRestartPC)
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 () () ()\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R75\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>?R'75\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 8. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 10. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>pc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R75 ()) (?Q'93 pc) (corrupt_tcb_intent obj_id') (as_user obj_id' (setRegister NextIP pc))
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?R'75 ()\<rbrace> as_user obj_id' getRestartPC \<lbrace>?Q'93\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; ?R'75 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> as_user obj_id' getRestartPC \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; False\<rbrakk> \<Longrightarrow> no_fail (?R'75 ()) (as_user obj_id' getRestartPC)
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 () () ()\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R75\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>?R'75\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 8. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 10. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?R'75 ()\<rbrace> as_user obj_id' getRestartPC \<lbrace>\<lambda>pc a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a\<rbrace>
 2. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; ?R'75 () s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> as_user obj_id' getRestartPC \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c; False\<rbrakk> \<Longrightarrow> no_fail (?R'75 ()) (as_user obj_id' getRestartPC)
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 () () ()\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>?R'75\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 7. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 8. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 10. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and ?Q86 y ya yb and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
A total of 15 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>\<lambda>a b. valid_idle b \<and> not_idle_thread obj_id' b \<and> valid_etcbs b\<rbrace>
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and ?Q'84 y ya yc and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> set frame_registers \<subseteq> UNIV
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 y ya yb) (?Q'62 y ya yc) (corrupt_tcb_intent obj_id') (when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od))
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (10 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b False d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b False d 0; \<not> c\<rbrakk> \<Longrightarrow> dcorres dc (?Q60 () () ()) (?Q'62 () () ()) (corrupt_tcb_intent obj_id') (return ())
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and ?Q60 y ya yb and ?Q51 y ya yb\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and ?Q'62 y ya yc and ?Q'53 y ya yc\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?R49 y ya yb yc rv) (?R'49 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv >>= return) (do y <- when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R49 y ya yb yc\<rbrace>
 3. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>?R'49 y ya yb yc\<rbrace>
 4. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 5. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (12 subgoals):
 1. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> dcorres dc (?P128 y ya yb yc rv) (?P'130 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters))
 2. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 4. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. ?P128 y ya yb yc rv and ?Q129 y ya yb yc rv\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. ?P'130 y ya yb yc yd and ?Q'131 y ya yb yc yd\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; d\<rbrakk> \<Longrightarrow> dcorres dc (?P137 y ya yb yc rv) (?P'139 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters))
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; \<not> d\<rbrakk> \<Longrightarrow> dcorres dc (?Q138 y ya yb yc rv) (?Q'140 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters))
 3. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 5. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. ?P137 y ya yb yc rv and ?Q138 y ya yb yc rv and ?Q129 y ya yb yc rv\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. ?P'139 y ya yb yc yd and ?Q'140 y ya yb yc yd and ?Q'131 y ya yb yc yd\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 9. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c True e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c True 0; d\<rbrakk> \<Longrightarrow> dcorres dc (?P137 () () () () ()) (?P'139 () () () () ()) (corrupt_tcb_intent obj_id') (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters)
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; \<not> d\<rbrakk> \<Longrightarrow> dcorres dc (?Q138 y ya yb yc rv) (?Q'140 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters))
 3. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 4. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 5. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. ?P137 y ya yb yc rv and ?Q138 y ya yb yc rv and ?Q129 y ya yb yc rv\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. ?P'139 y ya yb yc yd and ?Q'140 y ya yb yc yd and ?Q'131 y ya yb yc yd\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 9. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; \<not> d\<rbrakk> \<Longrightarrow> dcorres dc (?Q138 y ya yb yc rv) (?Q'140 y ya yb yc yd) (K_bind (corrupt_tcb_intent obj_id') rv) (when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters))
 2. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 4. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and ?Q138 y ya yb yc rv and ?Q129 y ya yb yc rv\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and ?Q'140 y ya yb yc yd and ?Q'131 y ya yb yc yd\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c False e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c False 0; \<not> d\<rbrakk> \<Longrightarrow> dcorres dc (?Q138 () () () () ()) (?Q'140 () () () () ()) (corrupt_tcb_intent obj_id') (return ())
 2. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 4. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and ?Q138 y ya yb yc rv and ?Q129 y ya yb yc rv\<rbrace>
 6. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and ?Q'140 y ya yb yc yd and ?Q'131 y ya yb yc yd\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 8. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 10. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?R'127 y ya yb yc rv yd ye) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 3. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 4. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 5. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
 6. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 7. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 9. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 10. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R127 y ya yb yc rv yd x) (?Q'149 y ya yb yc rv yd x ye cur) (return x) (do y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?R'127 y ya yb yc rv yd ye\<rbrace> gets cur_thread \<lbrace>?Q'149 y ya yb yc rv yd x ye\<rbrace>
 3. \<And>y ya yb yc rv yd x ye s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; ?R'127 y ya yb yc rv yd ye s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; False\<rbrakk> \<Longrightarrow> no_fail (?R'127 y ya yb yc rv yd ye) (gets cur_thread)
 5. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>?R127 y ya yb yc rv yd\<rbrace>
 6. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 7. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 8. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
 9. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
 10. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'53 y ya yc\<rbrace>
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when (obj_id' = cur) reschedule_required)
 2. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R156 y ya yb yc rv yd x) (?R'154 y ya yb yc rv yd x ye cur) (return x) (return [])
 3. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?Q'154 y ya yb yc rv yd x ye cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'154 y ya yb yc rv yd x ye cur\<rbrace>
 4. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?R'127 y ya yb yc rv yd ye\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'154 y ya yb yc rv yd x ye cur\<rbrace>
 5. \<And>y ya yb yc rv yd x ye s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; ?R'127 y ya yb yc rv yd ye s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; False\<rbrakk> \<Longrightarrow> no_fail (?R'127 y ya yb yc rv yd ye) (gets cur_thread)
 7. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R156 y ya yb yc rv yd x\<rbrace>
 8. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 10. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when (obj_id' = cur) reschedule_required)
 2. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R156 y ya yb yc rv yd x) (?R'154 y ya yb yc rv yd x ye cur) (return x) (return [])
 3. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?Q'154 y ya yb yc rv yd x ye cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'154 y ya yb yc rv yd x ye cur\<rbrace>
 4. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?R'127 y ya yb yc rv yd ye\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'154 y ya yb yc rv yd x ye cur\<rbrace>
 5. \<And>y ya yb yc rv yd x ye s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; ?R'127 y ya yb yc rv yd ye s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; False\<rbrakk> \<Longrightarrow> no_fail (?R'127 y ya yb yc rv yd ye) (gets cur_thread)
 7. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R156 y ya yb yc rv yd x\<rbrace>
 8. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 10. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) reschedule_required
 2. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R156 y ya yb yc rv yd x) (?R'154 y ya yb yc rv yd x ye cur) (return x) (return [])
 3. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?Q'154 y ya yb yc rv yd x ye cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'154 y ya yb yc rv yd x ye cur\<rbrace>
 4. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?R'127 y ya yb yc rv yd ye\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'154 y ya yb yc rv yd x ye cur\<rbrace>
 5. \<And>y ya yb yc rv yd x ye s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; ?R'127 y ya yb yc rv yd ye s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; False\<rbrakk> \<Longrightarrow> no_fail (?R'127 y ya yb yc rv yd ye) (gets cur_thread)
 7. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R156 y ya yb yc rv yd x\<rbrace>
 8. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 10. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> dcorres dc (?R156 y ya yb yc rv yd x) (?R'154 y ya yb yc rv yd x ye cur) (return x) (return [])
 2. \<And>y ya yb yc rv yd x ye cur. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?Q'154 y ya yb yc rv yd x ye cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'154 y ya yb yc rv yd x ye cur\<rbrace>
 3. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye\<rbrakk> \<Longrightarrow> \<lbrace>?R'127 y ya yb yc rv yd ye\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'154 y ya yb yc rv yd x ye cur\<rbrace>
 4. \<And>y ya yb yc rv yd x ye s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; ?R'127 y ya yb yc rv yd ye s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>y ya yb yc rv yd x ye. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd; dc x ye; False\<rbrakk> \<Longrightarrow> no_fail (?R'127 y ya yb yc rv yd ye) (gets cur_thread)
 6. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q129 y ya yb yc rv\<rbrace> K_bind (corrupt_tcb_intent obj_id') rv \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R156 y ya yb yc rv yd x\<rbrace>
 7. \<And>y ya yb yc rv yd. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc; dc rv yd\<rbrakk> \<Longrightarrow> \<lbrace>?Q'131 y ya yb yc yd\<rbrace> when d (mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) gpRegisters) \<lbrace>?R'127 y ya yb yc rv yd\<rbrace>
 8. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q51 y ya yb\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>a. True) and ?Q129 y ya yb yc rv\<rbrace>
 9. \<And>y ya yb yc. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'53 y ya yc\<rbrace> when c (do y <- mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers;
pc <- as_user obj_id' getRestartPC;
as_user obj_id' (setNextPC pc)
od) \<lbrace>\<lambda>yd. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and ?Q'131 y ya yb yc yd\<rbrace>
 10. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and ?Q51 y ya yb\<rbrace>
A total of 15 subgoals... proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> \<lbrace>?Q268 () () ()\<rbrace> mapM_x (\<lambda>r. do v <- as_user target_id' (getRegister r);
as_user obj_id' (setRegister r v)
od) frame_registers \<lbrace>\<lambda>x s. tcb_at obj_id' s \<and> tcb_at target_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> not_idle_thread target_id' s \<and> valid_etcbs s \<and> tcb_at obj_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_etcbs s\<rbrace>
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>s. True \<and> True \<and> True \<and> K (?P251 y ya yb) s)\<rbrace>
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and (if c then ?Q268 y ya yc else (\<lambda>s. tcb_at obj_id' s \<and> tcb_at target_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> not_idle_thread target_id' s \<and> valid_etcbs s \<and> (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) s \<and> True \<and> True))\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b True d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b True d 0; c\<rbrakk> \<Longrightarrow> set frame_registers \<subseteq> UNIV
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>s. True \<and> True \<and> True \<and> K (?P251 y ya yb) s)\<rbrace>
 3. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and (if c then \<lambda>a. tcb_at obj_id' a \<and> tcb_at target_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> not_idle_thread target_id' a \<and> valid_etcbs a \<and> tcb_at obj_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a else (\<lambda>s. tcb_at obj_id' s \<and> tcb_at target_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> not_idle_thread target_id' s \<and> valid_etcbs s \<and> (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) s \<and> True \<and> True))\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 5. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 y\<rbrace> Tcb_D.restart obj_id' \<sqinter> return () \<lbrace>\<lambda>yb. (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>s. True \<and> True \<and> True \<and> K (?P251 y ya yb) s)\<rbrace>
 2. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and (if c then \<lambda>a. tcb_at obj_id' a \<and> tcb_at target_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> not_idle_thread target_id' a \<and> valid_etcbs a \<and> tcb_at obj_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a else (\<lambda>s. tcb_at obj_id' s \<and> tcb_at target_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> not_idle_thread target_id' s \<and> valid_etcbs s \<and> (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) s \<and> True \<and> True))\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ?Q25 y\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ya\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc. tcb_at obj_id' and tcb_at target_id' and valid_idle and not_idle_thread obj_id' and not_idle_thread target_id' and valid_etcbs and (\<lambda>a. valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a) and (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) and (if c then \<lambda>a. tcb_at obj_id' a \<and> tcb_at target_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> not_idle_thread target_id' a \<and> valid_etcbs a \<and> tcb_at obj_id' a \<and> valid_idle a \<and> not_idle_thread obj_id' a \<and> valid_etcbs a else (\<lambda>s. tcb_at obj_id' s \<and> tcb_at target_id' s \<and> valid_idle s \<and> not_idle_thread obj_id' s \<and> not_idle_thread target_id' s \<and> valid_etcbs s \<and> (tcb_at obj_id' and valid_idle and not_idle_thread obj_id' and valid_etcbs) s \<and> True \<and> True))\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ((\<lambda>s. True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> K (?P357 y) s) and ((\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>s. True \<and> True \<and> True \<and> K (?P357 y) s)))\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 4. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ()\<rbrace> when b (Tcb_A.restart obj_id') \<lbrace>\<lambda>yc x. valid_idle x \<and> not_idle_thread obj_id' x \<and> not_idle_thread target_id' x \<and> tcb_at obj_id' x \<and> tcb_at target_id' x \<and> valid_etcbs x\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> Tcb_D.suspend target_id' \<sqinter> return () \<lbrace>\<lambda>y. (\<lambda>a. True) and (\<lambda>a. True) and ((\<lambda>s. True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> K (?P357 y) s) and ((\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>a. True) and (\<lambda>s. True \<and> True \<and> True \<and> K (?P357 y) s)))\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> when a (IpcCancel_A.suspend target_id') \<lbrace>\<lambda>ya. invs and tcb_at obj_id' and not_idle_thread obj_id' and valid_etcbs and (\<lambda>a. True) and ?Q'27 ya\<rbrace>
 4. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e; t = cdl_tcb_invocation.CopyRegisters obj_id' target_id' a b c d 0; (invs and tcb_at obj_id' and tcb_at target_id' and (tcb_at obj_id' and tcb_at target_id' and ex_nonz_cap_to target_id' and ex_nonz_cap_to obj_id') and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (normal_tcb_at target_id' and invs and valid_etcbs and (\<lambda>_. True) and ?Q'5) s proof (prove)
goal:
No subgoals!