theory Ipc_R

lemma handleFault_corres:
  "fr f f' \<Longrightarrow>
   corres dc (einvs and  st_tcb_at active thread and ex_nonz_cap_to thread
                   and (%_. valid_fault f))
             (invs' and sch_act_not thread
                    and (\<lambda>s. \<forall>p. thread \<notin> set(ksReadyQueues s p))
                    and st_tcb_at' simple' thread and ex_nonz_cap_to' thread)
             (handle_fault thread f) (handleFault thread f')" apply (simp add: handle_fault_def handleFault_def) apply (rule corres_guard_imp) apply (subst return_bind [symmetric],
               rule corres_split[where P="tcb_at thread",
                                  OF gets_the_noop_corres [where x="()"]]) apply (simp add: tcb_at_def) apply (rule corres_split_catch) apply (rule_tac F="valid_fault f" in corres_gen_asm) apply (rule sendFaultIPC_corres, assumption) apply simp apply (rule handleDoubleFault_corres) apply wp+ apply (rule hoare_post_impErr, rule sfi_invs_plus', simp_all)[1] apply clarsimp apply wp+ apply (clarsimp simp: st_tcb_at_tcb_at st_tcb_def2 invs_def
                         valid_state_def valid_idle_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fr f f' \<Longrightarrow> corres dc (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) (invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) (handle_fault thread f) (handleFault thread f') proof (prove)
goal (1 subgoal):
 1. f' = fault_map f \<Longrightarrow> corres dc (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) (do _ <- gets_the (get_tcb thread);
send_fault_ipc thread f <catch> handle_double_fault thread f
od) (sendFaultIPC thread (fault_map f) <catch> handleDoubleFault thread (fault_map f)) proof (prove)
goal (3 subgoals):
 1. f' = fault_map f \<Longrightarrow> corres dc ?Q1 ?Q'1 (do _ <- gets_the (get_tcb thread);
send_fault_ipc thread f <catch> handle_double_fault thread f
od) (sendFaultIPC thread (fault_map f) <catch> handleDoubleFault thread (fault_map f))
 2. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>f' = fault_map f; tcb_at thread s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None
 2. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 uu_) (?R'8 rv') (send_fault_ipc thread f <catch> handle_double_fault thread f) (sendFaultIPC thread (fault_map f) <catch> handleDoubleFault thread (fault_map f))
 3. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>?R8\<rbrace>
 4. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>?R'8\<rbrace>
 5. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 6. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 uu_) (?R'8 rv') (send_fault_ipc thread f <catch> handle_double_fault thread f) (sendFaultIPC thread (fault_map f) <catch> handleDoubleFault thread (fault_map f))
 2. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>?R8\<rbrace>
 3. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 5. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> corres (?f15 uu_ rv' \<oplus> dc) (?P16 uu_) (?P'18 rv') (send_fault_ipc thread f) (sendFaultIPC thread (fault_map f))
 2. \<And>uu_ rv' ft ft'. \<lbrakk>f' = fault_map f; dc uu_ rv'; ?f15 uu_ rv' ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E15 uu_ rv' ft) (?E'15 uu_ rv' ft') (handle_double_fault thread f ft) (handleDoubleFault thread (fault_map f) ft')
 3. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 uu_\<rbrace> send_fault_ipc thread f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E15 uu_ rv'\<rbrace>
 4. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'15 uu_ rv'\<rbrace>
 5. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_. ?P16 uu_ and ?Q17 uu_\<rbrace>
 6. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. ?P'18 rv' and ?Q'19 rv'\<rbrace>
 7. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 8. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'; valid_fault f\<rbrakk> \<Longrightarrow> corres (?f15 uu_ rv' \<oplus> dc) (?P25 uu_) (?P'18 rv') (send_fault_ipc thread f) (sendFaultIPC thread (fault_map f))
 2. \<And>uu_ rv' ft ft'. \<lbrakk>f' = fault_map f; dc uu_ rv'; ?f15 uu_ rv' ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E15 uu_ rv' ft) (?E'15 uu_ rv' ft') (handle_double_fault thread f ft) (handleDoubleFault thread (fault_map f) ft')
 3. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 uu_\<rbrace> send_fault_ipc thread f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E15 uu_ rv'\<rbrace>
 4. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'15 uu_ rv'\<rbrace>
 5. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_. ?P25 uu_ and (\<lambda>s. valid_fault f) and ?Q17 uu_\<rbrace>
 6. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. ?P'18 rv' and ?Q'19 rv'\<rbrace>
 7. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 8. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'; valid_fault f\<rbrakk> \<Longrightarrow> fr f (fault_map f)
 2. \<And>uu_ rv' ft ft'. \<lbrakk>f' = fault_map f; dc uu_ rv'; fr ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E15 uu_ rv' ft) (?E'15 uu_ rv' ft') (handle_double_fault thread f ft) (handleDoubleFault thread (fault_map f) ft')
 3. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 uu_\<rbrace> send_fault_ipc thread f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E15 uu_ rv'\<rbrace>
 4. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'15 uu_ rv'\<rbrace>
 5. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and ?Q17 uu_\<rbrace>
 6. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and ?Q'19 rv'\<rbrace>
 7. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 8. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>uu_ rv' ft ft'. \<lbrakk>f' = fault_map f; dc uu_ rv'; fr ft ft'\<rbrakk> \<Longrightarrow> corres dc (?E15 uu_ rv' ft) (?E'15 uu_ rv' ft') (handle_double_fault thread f ft) (handleDoubleFault thread (fault_map f) ft')
 2. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 uu_\<rbrace> send_fault_ipc thread f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E15 uu_ rv'\<rbrace>
 3. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'15 uu_ rv'\<rbrace>
 4. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and ?Q17 uu_\<rbrace>
 5. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and ?Q'19 rv'\<rbrace>
 6. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 7. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 uu_\<rbrace> send_fault_ipc thread f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft. tcb_at thread\<rbrace>
 2. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and ?Q17 uu_\<rbrace>
 4. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and ?Q'19 rv'\<rbrace>
 5. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 6. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>f' = fault_map f; dc uu_ rv'\<rbrakk> \<Longrightarrow> \<lbrace>?P'49 rv'\<rbrace> sendFaultIPC thread (fault_map f) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and (\<lambda>s. tcb_at thread s \<and> True)\<rbrace>
 3. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> ?P'49 rv' s)\<rbrace>
 4. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 5. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>f' = fault_map f; invs' s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> ksIdleThread s \<noteq> thread\<rbrakk> \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s
 2. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and (\<lambda>s. tcb_at thread s \<and> True)\<rbrace>
 3. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread) s)\<rbrace>
 4. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 5. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. f' = fault_map f \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>_. einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and (\<lambda>s. tcb_at thread s \<and> True)\<rbrace>
 2. f' = fault_map f \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return () \<lbrace>\<lambda>rv'. invs' and sch_act_not thread and tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread) s)\<rbrace>
 3. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q8) s
 4. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>f' = fault_map f; (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) s\<rbrakk> \<Longrightarrow> (tcb_at thread and (\<lambda>s. get_tcb thread s \<noteq> None \<longrightarrow> (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>s. valid_fault f) and (\<lambda>s. tcb_at thread s \<and> True)) s)) s
 2. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and (invs' and sch_act_not thread and tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>f' = fault_map f; (invs' and sch_act_not thread and (\<lambda>s. \<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) s\<rbrakk> \<Longrightarrow> (?P'8 and (invs' and sch_act_not thread and tcb_at' thread and (\<lambda>s. tcb_at' thread s \<and> (invs' and st_tcb_at' simple' thread and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread) s))) s proof (prove)
goal:
No subgoals!