theory IpcCancel_AI

lemma cancel_all_ipc_invs_helper:
  assumes x: "\<And>x ko. (x, symreftype k) \<in> refs_of ko
                \<Longrightarrow> (refs_of ko = {(x, symreftype k)} \<or>
                          (\<exists>y. refs_of ko = {(x, symreftype k), (y, TCBBound)}))"
  shows
  "\<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace>
     do y \<leftarrow> set_endpoint p Structures_A.endpoint.IdleEP;
        y \<leftarrow> mapM_x (\<lambda>t. do y \<leftarrow> set_thread_state t Structures_A.thread_state.Restart;
                           do_extended_op (tcb_sched_action (tcb_sched_enqueue) t) od) q;
        do_extended_op reschedule_required
    od \<lbrace>\<lambda>rv. invs\<rbrace>" apply (subst bind_assoc[symmetric]) apply (rule hoare_seq_ext) apply wp apply simp apply (rule hoare_pre) apply (wp cancel_all_invs_helper hoare_vcg_const_Ball_lift valid_irq_node_typ valid_ioports_lift) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_ep_def live_def) apply (rule conjI) apply (fastforce simp: live_def is_ep_def elim!: obj_at_weakenE split: kernel_object.splits) apply (rule conjI) apply clarsimp apply (drule(1) sym_refs_obj_atD, clarsimp) apply (drule(1) bspec, erule(1) if_live_then_nonz_capD) apply (rule refs_of_live, clarsimp) apply (rule conjI[rotated]) apply (subgoal_tac "\<exists>ep. ko_at (Endpoint ep) p s", clarsimp) apply (subgoal_tac "\<exists>rt. (x, rt) \<in> ep_q_refs_of ep", clarsimp) apply (fastforce elim!: ep_queued_st_tcb_at) apply (clarsimp simp: obj_at_def is_ep_def)+ apply (case_tac ko, simp_all) apply (frule(1) sym_refs_obj_atD) apply (frule obj_at_state_refs_ofD) apply (clarsimp dest!:obj_at_conj_distrib) apply (thin_tac "obj_at (\<lambda>ko. refs_of ko = set q \<times> {k}) p s") apply (erule delta_sym_refs) apply (clarsimp simp: if_split_asm)+ apply (safe) apply (fastforce dest!:symreftype_inverse' ep_no_ntfn_bound) apply (clarsimp dest!: symreftype_inverse') apply (frule (3) ep_list_tcb_at) apply (frule_tac t=y in tcb_at_no_ntfn_bound, simp+)[1] apply simp subgoal apply (clarsimp dest!: symreftype_inverse') apply (frule (3) ep_list_tcb_at) by (clarsimp simp: obj_at_def is_tcb is_ep) apply (fastforce dest!: obj_at_state_refs_ofD x) apply (fastforce dest!: obj_at_state_refs_ofD x) apply (fastforce dest!: symreftype_inverse' ep_no_ntfn_bound) apply (clarsimp) apply (fastforce dest!: symreftype_inverse' ep_no_ntfn_bound) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace> do y <- set_endpoint p IdleEP;
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q;
do_extended_op reschedule_required
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace> do y <- do y <- set_endpoint p IdleEP;
mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q
od;
do_extended_op reschedule_required
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?B y\<rbrace> do_extended_op reschedule_required \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace> do y <- set_endpoint p IdleEP;
mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q
od \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y s f. invs (trans_state f s) = invs s
 2. \<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace> do y <- set_endpoint p IdleEP;
mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q
od \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p\<rbrace> do y <- set_endpoint p IdleEP;
mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q
od \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> do y <- set_endpoint p IdleEP;
mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) q
od \<lbrace>\<lambda>y. invs\<rbrace>
 2. \<And>s. (invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint IdleEP) and K (is_simple_type (Endpoint IdleEP))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> (if_live_then_nonz_cap s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to p s)) \<and> zombies_final s \<and> valid_mdb s \<and> (obj_at (\<lambda>ko. partial_inv Endpoint ko \<noteq> None) p and valid_idle) s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> (\<forall>x\<in>set q. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> ((state_refs_of s)(p := ep_q_refs_of IdleEP)) x. snd r = TCBBound} else ((state_refs_of s)(p := ep_q_refs_of IdleEP)) x) \<and> sym_refs (state_hyp_refs_of s) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) p s \<and> (\<forall>x\<in>set q. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) p s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set q. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set q. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set q. ex_nonz_cap_to x s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; x \<in> set q\<rbrakk> \<Longrightarrow> ex_nonz_cap_to x s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s x ko. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; x \<in> set q; is_ep ko; refs_of ko = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to x s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s x ko obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; x \<in> set q; is_ep ko; refs_of ko = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (p, symreftype k) \<in> refs_of obj; kheap s x = Some obj\<rbrakk> \<Longrightarrow> live obj
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) \<and> (\<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set q. st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (3 subgoals):
 1. \<And>s x ep. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; x \<in> set q; ko_at (Endpoint ep) p s\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> \<exists>ep. ko_at (Endpoint ep) p s
 3. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (4 subgoals):
 1. \<And>s x ep rt. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; x \<in> set q; ko_at (Endpoint ep) p s; (x, rt) \<in> ep_q_refs_of ep\<rbrakk> \<Longrightarrow> st_tcb_at (Not \<circ> (halted or awaiting_reply)) x s
 2. \<And>s x ep. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; x \<in> set q; ko_at (Endpoint ep) p s\<rbrakk> \<Longrightarrow> \<exists>rt. (x, rt) \<in> ep_q_refs_of ep
 3. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> \<exists>ep. ko_at (Endpoint ep) p s
 4. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (3 subgoals):
 1. \<And>s x ep. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; x \<in> set q; ko_at (Endpoint ep) p s\<rbrakk> \<Longrightarrow> \<exists>rt. (x, rt) \<in> ep_q_refs_of ep
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> \<exists>ep. ko_at (Endpoint ep) p s
 3. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; kheap s p = Some ko; case ko of Endpoint p \<Rightarrow> True | _ \<Rightarrow> False; refs_of ko = set q \<times> {k}\<rbrakk> \<Longrightarrow> \<exists>ep. ko = Endpoint ep
 2. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; \<exists>ko. (is_ep ko \<and> refs_of ko = set q \<times> {k}) \<and> state_refs_of s p = refs_of ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; obj_at (\<lambda>ko. is_ep ko \<and> refs_of ko = set q \<times> {k}) p s; \<exists>ko. (is_ep ko \<and> refs_of ko = set q \<times> {k}) \<and> state_refs_of s p = refs_of ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s); \<exists>ko. (is_ep ko \<and> refs_of ko = set q \<times> {k}) \<and> state_refs_of s p = refs_of ko\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>s ko koa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; obj_at (\<lambda>ko. refs_of ko = set q \<times> {k}) p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>s ko koa. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> (if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x); (y, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y \<in> set q then {r \<in> if y = p then {} else state_refs_of s y. snd r = TCBBound} else if y = p then {} else state_refs_of s y)
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x \<in> set q then {r \<in> if x = p then {} else state_refs_of s x. snd r = TCBBound} else if x = p then {} else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y \<in> set q then {r \<in> if y = p then {} else state_refs_of s y. snd r = TCBBound} else if y = p then {} else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q \<and> (x = p \<or> tp \<noteq> TCBBound) \<or> x \<notin> set q \<and> x = p; y \<in> set q \<or> y \<noteq> p \<and> (y = p \<or> (x, symreftype tp) \<in> state_refs_of s y)\<rbrakk> \<Longrightarrow> y \<in> set q \<and> (y = p \<or> y \<noteq> p \<and> (x, symreftype tp) \<notin> state_refs_of s y \<or> symreftype tp \<noteq> TCBBound) proof (prove)
goal (9 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<in> set q; tp \<noteq> TCBBound; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 7. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 8. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 9. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<in> set q; tp \<noteq> TCBBound; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 7. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 8. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>s ko koa x y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, NTFNBound) \<in> state_refs_of s x; x \<in> set q; y \<in> set q; y \<noteq> p; (x, TCBBound) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 7. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 8. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>s ko koa x y. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, NTFNBound) \<in> state_refs_of s x; x \<in> set q; y \<in> set q; y \<noteq> p; (x, TCBBound) \<in> state_refs_of s y; tcb_at x s\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 7. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 8. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 7. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<in> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 6. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s_; pspace_aligned s_; pspace_distinct s_; if_live_then_nonz_cap s_; zombies_final s_; sym_refs (state_hyp_refs_of s_); valid_mdb s_; valid_ioc s_; valid_idle s_; only_idle s_; if_unsafe_then_cap s_; valid_reply_caps s_; valid_reply_masters s_; valid_global_refs s_; valid_arch_state s_; valid_irq_node s_; valid_irq_handlers s_; valid_irq_states s_; valid_ioports s_; valid_machine_state s_; valid_vspace_objs s_; valid_arch_caps s_; valid_global_objs s_; valid_kernel_mappings s_; equal_kernel_mappings s_; valid_asid_map s_; valid_global_vspace_mappings s_; pspace_in_kernel_window s_; cap_refs_in_kernel_window s_; pspace_respects_device_region s_; cap_refs_respects_device_region s_; cur_tcb s_; ep_at p s_; is_ep ko_; is_ep koa_; refs_of ko_ = set q \<times> {k}; refs_of koa_ = set q \<times> {k}; state_refs_of s_ p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s_; (y_, tp_) \<in> state_refs_of s_ p; p \<in> set q; y_ \<noteq> p; (p, symreftype tp_) \<in> state_refs_of s_ y_; y_ \<noteq> p; symreftype tp_ = TCBBound; \<not> False; (p, symreftype tp_) \<in> state_refs_of s_ y_\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s_; pspace_aligned s_; pspace_distinct s_; if_live_then_nonz_cap s_; zombies_final s_; sym_refs (state_hyp_refs_of s_); valid_mdb s_; valid_ioc s_; valid_idle s_; only_idle s_; if_unsafe_then_cap s_; valid_reply_caps s_; valid_reply_masters s_; valid_global_refs s_; valid_arch_state s_; valid_irq_node s_; valid_irq_handlers s_; valid_irq_states s_; valid_ioports s_; valid_machine_state s_; valid_vspace_objs s_; valid_arch_caps s_; valid_global_objs s_; valid_kernel_mappings s_; equal_kernel_mappings s_; valid_asid_map s_; valid_global_vspace_mappings s_; pspace_in_kernel_window s_; cap_refs_in_kernel_window s_; pspace_respects_device_region s_; cap_refs_respects_device_region s_; cur_tcb s_; ep_at p s_; is_ep ko_; is_ep koa_; refs_of ko_ = set q \<times> {NTFNBound}; refs_of koa_ = set q \<times> {NTFNBound}; state_refs_of s_ p = set q \<times> {NTFNBound}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, TCBBound) \<in> refs_of ko) x s_; p \<in> set q; y_ \<noteq> p; (p, TCBBound) \<in> state_refs_of s_ y_; k = NTFNBound; y_ \<in> set q; tp_ = NTFNBound\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s_; pspace_aligned s_; pspace_distinct s_; if_live_then_nonz_cap s_; zombies_final s_; sym_refs (state_hyp_refs_of s_); valid_mdb s_; valid_ioc s_; valid_idle s_; only_idle s_; if_unsafe_then_cap s_; valid_reply_caps s_; valid_reply_masters s_; valid_global_refs s_; valid_arch_state s_; valid_irq_node s_; valid_irq_handlers s_; valid_irq_states s_; valid_ioports s_; valid_machine_state s_; valid_vspace_objs s_; valid_arch_caps s_; valid_global_objs s_; valid_kernel_mappings s_; equal_kernel_mappings s_; valid_asid_map s_; valid_global_vspace_mappings s_; pspace_in_kernel_window s_; cap_refs_in_kernel_window s_; pspace_respects_device_region s_; cap_refs_respects_device_region s_; cur_tcb s_; ep_at p s_; is_ep ko_; is_ep koa_; refs_of ko_ = set q \<times> {NTFNBound}; refs_of koa_ = set q \<times> {NTFNBound}; state_refs_of s_ p = set q \<times> {NTFNBound}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, TCBBound) \<in> refs_of ko) x s_; p \<in> set q; y_ \<noteq> p; (p, TCBBound) \<in> state_refs_of s_ y_; k = NTFNBound; y_ \<in> set q; tp_ = NTFNBound; tcb_at p s_\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 5. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s x; x \<in> set q; y \<noteq> p; tp \<noteq> TCBBound; (x, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 4. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<in> set q; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 3. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> y \<in> set q
 2. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ko koa x y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ep_at p s; is_ep ko; is_ep koa; refs_of ko = set q \<times> {k}; refs_of koa = set q \<times> {k}; state_refs_of s p = set q \<times> {k}; \<forall>x\<in>set q. obj_at (\<lambda>ko. (p, symreftype k) \<in> refs_of ko) x s; (y, tp) \<in> state_refs_of s p; p \<notin> set q; y \<noteq> p; (p, symreftype tp) \<in> state_refs_of s y; y \<noteq> p; symreftype tp = TCBBound; \<not> False; (p, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!