theory Finalise_AI

lemma (in Finalise_AI_1) unbind_maybe_notification_invs:
  "\<lbrace>invs\<rbrace> unbind_maybe_notification ntfnptr \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: unbind_maybe_notification_def invs_def valid_state_def valid_pspace_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wpsimp wp: valid_irq_node_typ set_simple_ko_valid_objs valid_ioports_lift) apply simp apply safe defer 3 defer 6 apply (auto elim!: obj_at_weakenE obj_at_valid_objsE if_live_then_nonz_capD2
                   simp: live_def valid_ntfn_set_bound_None is_ntfn valid_obj_def)[6] apply (rule delta_sym_refs, assumption) apply (fastforce simp: obj_at_def is_tcb
                   dest!: pred_tcb_at_tcb_at ko_at_state_refs_ofD
                   split: if_split_asm) apply (clarsimp split: if_split_asm) apply (subst (asm) ko_at_state_refs_ofD, assumption) apply (fastforce simp: ntfn_q_refs_no_NTFNBound symreftype_inverse'  is_tcb refs_of_rev
                  dest!: refs_in_ntfn_q_refs) apply (rule delta_sym_refs, assumption) apply (clarsimp split: if_split_asm) apply (subst (asm) ko_at_state_refs_ofD, assumption) apply (frule refs_in_ntfn_q_refs) apply (fastforce) apply (clarsimp split: if_split_asm) apply (frule_tac P="(=) (Some ntfnptr)" in ntfn_bound_tcb_at, simp_all add: obj_at_def)[1] apply (fastforce simp: ntfn_q_refs_no_NTFNBound tcb_at_no_ntfn_bound tcb_ntfn_is_bound_def
                          obj_at_def tcb_st_refs_no_TCBBound
                   dest!: pred_tcb_at_tcb_at bound_tcb_at_state_refs_ofD) apply (subst (asm) ko_at_state_refs_ofD, assumption) apply (fastforce simp: ntfn_q_refs_no_NTFNBound symreftype_inverse'  is_tcb refs_of_rev
                 dest!: refs_in_ntfn_q_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> unbind_maybe_notification ntfnptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb)\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb)) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb)) s \<Longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<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_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (valid_objs and valid_simple_obj (Notification (ntfn_set_bound_tcb ntfn None)) and K (is_simple_type (Notification (ntfn_set_bound_tcb ntfn None)))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (if_live_then_nonz_cap s \<and> (live (Notification (ntfn_set_bound_tcb ntfn None)) \<longrightarrow> ex_nonz_cap_to ntfnptr s)) \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = x then {r \<in> ((state_refs_of s)(ntfnptr := ntfn_q_refs_of (ntfn_obj (ntfn_set_bound_tcb ntfn None)) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_bound_tcb ntfn None)))) x. snd r \<noteq> TCBBound} else ((state_refs_of s)(ntfnptr := ntfn_q_refs_of (ntfn_obj (ntfn_set_bound_tcb ntfn None)) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_bound_tcb ntfn None)))) a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> (obj_at (\<lambda>ko. partial_inv Notification ko \<noteq> None) ntfnptr 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_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at (Notification ntfn) ntfnptr s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<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_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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 \<Longrightarrow> \<forall>x. (x = ntfnptr \<longrightarrow> ntfn_bound_tcb ntfn = Some ntfnptr \<longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s \<and> (live (Notification (ntfn_set_bound_tcb ntfn None)) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s) \<and> (x \<noteq> ntfnptr \<longrightarrow> ntfn_bound_tcb ntfn = Some x \<longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s \<and> (live (Notification (ntfn_set_bound_tcb ntfn None)) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s) proof (prove)
goal (8 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a)
 4. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 5. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 6. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 7. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a)
 8. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 4. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 5. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 6. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a)
 7. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 8. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (8 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 4. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
 5. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; live (Notification (ntfn_set_bound_tcb ntfn None))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ntfnptr s
 6. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 7. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a)
 8. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s a)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; (y, tp) \<in> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 3. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfnptr then {r \<in> ntfn_q_refs_of (ntfn_obj ntfn). snd r \<noteq> TCBBound} else state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; (y, tp) \<in> state_refs_of s ntfnptr; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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; ntfn_bound_tcb ntfn = Some ntfnptr; (y, tp) \<in> refs_of (Notification ntfn); (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> tp = TCBBound\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn) \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if a = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>(y, tp) \<notin> state_refs_of s ntfnptr; ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<and> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y))
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>(y, tp) \<notin> refs_of (Notification ntfn); ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<and> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y))
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>(y, tp) \<notin> refs_of (Notification ntfn); ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn); tp = NTFNSignal\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<and> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y))
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if xa = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = x then {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} else if y = ntfnptr then ntfn_q_refs_of (ntfn_obj ntfn) else state_refs_of s y) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, TCBBound) \<in> state_refs_of s x\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s y))
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y. \<lbrakk>kheap s ntfnptr = Some (Notification ntfn); 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, TCBBound) \<in> state_refs_of s x; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (x, NTFNBound) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s x) \<and> (y \<noteq> x \<longrightarrow> (x, NTFNBound) \<notin> state_refs_of s y))
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> state_refs_of s ntfnptr; (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; 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 \<noteq> ntfnptr; ntfn_bound_tcb ntfn = Some x; (y, tp) \<in> refs_of (Notification ntfn); (y, tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y = x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s x \<longrightarrow> symreftype tp = TCBBound) \<and> (y \<noteq> x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal:
No subgoals!