theory Orphanage

lemma invokeTCB_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_inv_wf' tinv s \<rbrace>
   invokeTCB tinv
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (case_tac tinv, simp_all) apply (clarsimp simp: invokeTCB_def) apply (wp, clarsimp) apply (clarsimp simp: invokeTCB_def) apply (wp, clarsimp) apply (wp tc_no_orphans) apply (clarsimp split: option.splits simp: msg_align_bits elim!:is_aligned_weaken) apply (rename_tac option) apply (case_tac option) apply ((wp | simp add: invokeTCB_def)+)[2] apply (wp writereg_no_orphans readreg_no_orphans copyreg_no_orphans settlsbase_no_orphans | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_inv_wf' tinv s\<rbrace> invokeTCB tinv \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. tinv = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x1 s \<and> ex_nonz_cap_to' x1 s\<rbrace> invokeTCB (tcbinvocation.Suspend x1) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x2. tinv = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x2 s \<and> ex_nonz_cap_to' x2 s\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. tinv = tcbinvocation.Suspend x1 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x1 s \<and> ex_nonz_cap_to' x1 s\<rbrace> liftE (do y <- ThreadDecls_H.suspend x1;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x2. tinv = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x2 s \<and> ex_nonz_cap_to' x2 s\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. tinv = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x2 s \<and> ex_nonz_cap_to' x2 s\<rbrace> invokeTCB (tcbinvocation.Resume x2) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x2. tinv = tcbinvocation.Resume x2 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x2 s \<and> ex_nonz_cap_to' x2 s\<rbrace> liftE (do y <- ThreadDecls_H.restart x2;
return []
od) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38. tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrace> invokeTCB (tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 x38 s. \<lbrakk>tinv = tcbinvocation.ThreadControl x31 x32 x33 x34 x35 x36 x37 x38; no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x31 s \<and> ex_nonz_cap_to' x31 s \<and> valid_option_prio x35 \<and> valid_option_prio x34 \<and> (case x36 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x36 of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (case x37 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x37 of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (case x38 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> cte_wp_at' (\<lambda>_. True) (snd x2)) s \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits) \<and> (case x38 of None \<Rightarrow> True | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2)) \<and> ((\<exists>a b. x36 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x37 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> ((\<exists>a b. x38 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) x32 s) \<and> (case x35 of None \<Rightarrow> True | Some (pr, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) pr) auth s) \<and> (case x34 of None \<Rightarrow> True | Some (m, auth) \<Rightarrow> mcpriority_tcb_at' ((\<le>) m) auth s)\<rbrakk> \<Longrightarrow> (no_orphans and invs' and sch_act_simple and tcb_at' x31 and ex_nonz_cap_to' x31 and (case x36 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x36 of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case x37 of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case x37 of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_cap' x) and K (case case x38 of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> True | Some x \<Rightarrow> isArchObjectCap x) and K (case x38 of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned 2 \<circ> fst) x) and K (case x38 of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x) and K (case x38 of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x) and K (valid_option_prio x35 \<and> valid_option_prio x34)) s
 2. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42. tinv = tcbinvocation.NotificationControl x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case x42 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 x42) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 option. tinv = tcbinvocation.NotificationControl x41 option \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 option) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x41 option. \<lbrakk>tinv = tcbinvocation.NotificationControl x41 option; option = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 option) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x41 option a. \<lbrakk>tinv = tcbinvocation.NotificationControl x41 option; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x41 s \<and> ex_nonz_cap_to' x41 s \<and> (case option of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) x41) s\<rbrace> invokeTCB (tcbinvocation.NotificationControl x41 option) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54. tinv = tcbinvocation.WriteRegisters x51 x52 x53 x54 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x51 s \<and> ex_nonz_cap_to' x51 s\<rbrace> invokeTCB (tcbinvocation.WriteRegisters x51 x52 x53 x54) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x61 x62 x63 x64. tinv = tcbinvocation.ReadRegisters x61 x62 x63 x64 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x61 s \<and> ex_nonz_cap_to' x61 s\<rbrace> invokeTCB (tcbinvocation.ReadRegisters x61 x62 x63 x64) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x71 x72 x73 x74 x75 x76 x77. tinv = tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x71 s \<and> tcb_at' x72 s \<and> ex_nonz_cap_to' x72 s \<and> ex_nonz_cap_to' x71 s\<rbrace> invokeTCB (tcbinvocation.CopyRegisters x71 x72 x73 x74 x75 x76 x77) \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>x81 x82. tinv = tcbinvocation.SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> tcb_at' x81 s \<and> ex_nonz_cap_to' x81 s\<rbrace> invokeTCB (tcbinvocation.SetTLSBase x81 x82) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal:
No subgoals!