theory KHeap_DR

lemma get_notification_pick:
  "\<lbrakk>kheap s epptr = Some (kernel_object.Notification notification);
    valid_state s\<rbrakk>
      \<Longrightarrow> valid_ntfn_abstract notification epptr s" apply (clarsimp simp:valid_ntfn_abstract_def) apply (rule conjI[rotated]) apply (case_tac "ntfn_obj notification") apply (clarsimp simp:valid_state_def valid_pspace_def sym_refs_def) apply (clarsimp simp:none_is_waiting_ntfn_def) apply (rule set_eqI) apply (clarsimp simp:ntfn_waiting_set_def) apply (drule_tac x=x in spec) apply (clarsimp simp: state_refs_of_def ntfn_bound_refs_def2) apply (clarsimp simp:valid_state_def valid_pspace_def valid_objs_def) apply (drule_tac x=epptr in bspec) apply (clarsimp simp:dom_def) apply (clarsimp simp:valid_obj_def valid_ntfn_def) apply (rule conjI) apply (rule sym) apply (rule antisym) apply (clarsimp simp:ntfn_waiting_set_def sym_refs_def) apply (drule_tac x = x in spec) apply (clarsimp simp:state_refs_of_def ntfn_bound_refs_def2) apply (clarsimp simp:ntfn_waiting_set_def sym_refs_def) apply (drule_tac x= epptr in spec) apply (clarsimp simp:state_refs_of_def ntfn_waiting_set_def ntfn_bound_refs_def2 split: option.splits) apply (drule_tac x= x in bspec) apply simp apply (clarsimp) apply (case_tac y) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
                 split:Structures_A.kernel_object.splits)+ apply (clarsimp simp: tcb_bound_refs_def2 split:Structures_A.thread_state.splits) apply (clarsimp simp:ntfn_waiting_set_def) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
               split:Structures_A.kernel_object.splits)+ apply (clarsimp simp: split:Structures_A.endpoint.splits) apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
              split:Structures_A.kernel_object.splits)+ apply (clarsimp simp: ntfn_bound_refs_def2 split:Structures_A.ntfn.splits) apply (clarsimp simp:refs_of_def tcb_bound_refs_def2 ntfn_bound_refs_def2 tcb_st_refs_of_def ep_q_refs_of_def ntfn_q_refs_of_def
             split:Structures_A.kernel_object.splits split: Structures_A.thread_state.splits Structures_A.endpoint.splits Structures_A.ntfn.splits)+ apply (subgoal_tac "ko_at (Notification notification) epptr s
                      \<and> ko_at (Notification notification) p' s") apply (clarsimp simp: neq_Nil_conv) apply (drule(1) sym_refs_ko_atD)+ apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_def2) apply (clarsimp simp: obj_at_def) apply (clarsimp simp:valid_state_def valid_pspace_def sym_refs_def) apply (clarsimp simp:none_is_waiting_ntfn_def) apply (rule set_eqI) apply (clarsimp simp:ntfn_waiting_set_def) apply (drule_tac x=x in spec) apply (clarsimp simp: state_refs_of_def ntfn_bound_refs_def2) apply (case_tac "ntfn_bound_tcb notification") apply (clarsimp simp: valid_state_def ntfn_bound_set_def valid_pspace_def) apply (drule_tac x=x in sym_refsD[rotated]) apply (fastforce simp: state_refs_of_def) apply (clarsimp simp: symreftype_inverse' state_refs_of_def ntfn_q_refs_no_NTFNBound) apply (clarsimp simp: ntfn_bound_set_def valid_state_def valid_pspace_def) apply (frule_tac x=epptr in sym_refsD[rotated]) apply (fastforce simp: state_refs_of_def) apply (clarsimp simp: symreftype_inverse' state_refs_of_def) apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (clarsimp simp: refs_of_def ntfn_q_refs_no_TCBBound tcb_st_refs_no_TCBBound tcb_bound_refs_def split: option.splits Structures_A.kernel_object.splits) apply clarsimp apply (drule_tac x=x in kheap_to_ko_at) apply (drule sym_refs_ko_atD, simp add: state_refs_of_def) apply (clarsimp split: option.splits) apply (drule_tac x=a in kheap_to_ko_at) apply (drule sym_refs_ko_atD, simp add: state_refs_of_def) apply (case_tac a) apply (simp_all add: ntfn_q_refs_no_TCBBound) apply (clarsimp simp: tcb_bound_refs_def2) apply (clarsimp simp: refs_of_def obj_at_def ntfn_q_refs_no_NTFNBound) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> valid_ntfn_abstract notification epptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s \<and> (case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = IdleNtfn\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = IdleNtfn; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> none_is_waiting_ntfn epptr s
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = IdleNtfn; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> ntfn_waiting_set epptr s = {}
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = IdleNtfn; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> (x \<in> ntfn_waiting_set epptr s) = (x \<in> {})
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = IdleNtfn; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = IdleNtfn; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = WaitingNtfn x2\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj 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_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\<rbrakk> \<Longrightarrow> x2 \<noteq> [] \<and> set x2 = ntfn_waiting_set epptr s \<and> (\<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p')
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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\<rbrakk> \<Longrightarrow> epptr \<in> dom (kheap s)
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; \<exists>obj. kheap s epptr = Some obj \<and> valid_obj epptr obj s\<rbrakk> \<Longrightarrow> x2 \<noteq> [] \<and> set x2 = ntfn_waiting_set epptr s \<and> (\<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p')
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; \<exists>obj. kheap s epptr = Some obj \<and> valid_obj epptr obj s\<rbrakk> \<Longrightarrow> x2 \<noteq> [] \<and> set x2 = ntfn_waiting_set epptr s \<and> (\<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p')
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 = ntfn_waiting_set epptr s \<and> (\<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p')
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 = ntfn_waiting_set epptr s
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> ntfn_waiting_set epptr s = set x2
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> ntfn_waiting_set epptr s \<subseteq> set x2
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 \<subseteq> ntfn_waiting_set epptr s
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> x \<in> set x2
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 \<subseteq> ntfn_waiting_set epptr s
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> x \<in> set x2
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 \<subseteq> ntfn_waiting_set epptr s
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> set x2 \<subseteq> ntfn_waiting_set epptr s
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; x \<in> set x2\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; x \<in> set x2; \<forall>x\<in>state_refs_of s epptr. case x of (y, tp) \<Rightarrow> (epptr, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x. \<lbrakk>\<forall>x\<in>set x2. (\<exists>y. kheap s x = Some y) \<and> (\<forall>x2. kheap s x = Some x2 \<longrightarrow> (epptr, TCBSignal) \<in> refs_of x2); kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (6 subgoals):
 1. \<And>x2 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2\<rbrakk> \<Longrightarrow> x \<in> set x2
 2. \<And>x2 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (\<exists>y. kheap s x = Some y) \<and> (\<forall>x2. kheap s x = Some x2 \<longrightarrow> (epptr, TCBSignal) \<in> refs_of x2)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 5. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 6. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (\<exists>y. kheap s x = Some y) \<and> (\<forall>x2. kheap s x = Some x2 \<longrightarrow> (epptr, TCBSignal) \<in> refs_of x2)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x y. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (9 subgoals):
 1. \<And>x2 x y x11 x12. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.CNode x11 x12\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x2 x y x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = TCB x2a\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2 x y x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 5. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 6. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 7. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 8. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 9. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (8 subgoals):
 1. \<And>x2 x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> (case tcb_state x2a of BlockedOnReceive x payl \<Rightarrow> {(x, TCBBlockedRecv)} | BlockedOnSend x payl \<Rightarrow> {(x, TCBBlockedSend)} | BlockedOnNotification x \<Rightarrow> {(x, TCBSignal)} | _ \<Rightarrow> {}) \<or> (epptr, TCBSignal) \<in> tcb_bound_refs (tcb_bound_notification x2a); kheap s x = Some (TCB x2a)\<rbrakk> \<Longrightarrow> tcb_state x2a = BlockedOnNotification epptr
 2. \<And>x2 x y x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 5. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 6. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 7. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 8. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (7 subgoals):
 1. \<And>x2 x y x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Endpoint x3\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 5. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 6. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 7. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (7 subgoals):
 1. \<And>x2 x x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> ep_q_refs_of x3; kheap s x = Some (kernel_object.Endpoint x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 5. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 6. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 7. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (7 subgoals):
 1. \<And>x2 x x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> (case x3 of IdleEP \<Rightarrow> {} | SendEP q \<Rightarrow> set q \<times> {EPSend} | RecvEP q \<Rightarrow> set q \<times> {EPRecv}); kheap s x = Some (kernel_object.Endpoint x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 5. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 6. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 7. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (6 subgoals):
 1. \<And>x2 x y x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = kernel_object.Notification x4\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 5. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 6. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (6 subgoals):
 1. \<And>x2 x x4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> (case ntfn_obj x4 of WaitingNtfn q \<Rightarrow> set q \<times> {NTFNSignal} | _ \<Rightarrow> {}) \<or> (epptr, TCBSignal) \<in> ntfn_bound_refs (ntfn_bound_tcb x4); kheap s x = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> False
 2. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 4. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 5. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 6. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (5 subgoals):
 1. \<And>x2 x y x5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ntfn_bound_tcb notification = None; x \<in> set x2; (epptr, TCBSignal) \<in> refs_of y; kheap s x = Some y; y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>t. y = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 2. \<And>x x2a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn [x]; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; tcb_at x s; ntfn_bound_tcb notification = Some x; kheap s x = Some x2a; (epptr, TCBBound) \<in> refs_of x2a; (epptr, TCBSignal) \<in> refs_of x2a\<rbrakk> \<Longrightarrow> \<exists>t. x2a = TCB t \<and> tcb_state t = BlockedOnNotification epptr
 3. \<And>x2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s\<rbrakk> \<Longrightarrow> \<forall>p'. Some (kernel_object.Notification notification) = kheap s p' \<longrightarrow> epptr = p'
 4. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 5. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'\<rbrakk> \<Longrightarrow> epptr = p'
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'; ko_at (kernel_object.Notification notification) epptr s \<and> ko_at (kernel_object.Notification notification) p' s\<rbrakk> \<Longrightarrow> epptr = p'
 2. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification notification) epptr s \<and> ko_at (kernel_object.Notification notification) p' s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>p' y ys. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn (y # ys); 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_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; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'; ko_at (kernel_object.Notification notification) epptr s; ko_at (kernel_object.Notification notification) p' s; tcb_at y s; \<forall>t\<in>set ys. tcb_at t s; y \<notin> set ys; distinct ys\<rbrakk> \<Longrightarrow> epptr = p'
 2. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification notification) epptr s \<and> ko_at (kernel_object.Notification notification) p' s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (4 subgoals):
 1. \<And>p' y ys. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn (y # ys); 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_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; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'; tcb_at y s; \<forall>t\<in>set ys. tcb_at t s; y \<notin> set ys; distinct ys; state_refs_of s epptr = refs_of (kernel_object.Notification notification) \<and> (\<forall>(x, tp)\<in>refs_of (kernel_object.Notification notification). obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s); state_refs_of s p' = refs_of (kernel_object.Notification notification) \<and> (\<forall>(x, tp)\<in>refs_of (kernel_object.Notification notification). obj_at (\<lambda>ko. (p', symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> epptr = p'
 2. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification notification) epptr s \<and> ko_at (kernel_object.Notification notification) p' s
 3. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 4. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x2 p'. \<lbrakk>kheap s epptr = kheap s p'; ntfn_obj notification = WaitingNtfn x2; 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_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; x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb notification of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb notification) s; Some (kernel_object.Notification notification) = kheap s p'\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification notification) epptr s \<and> ko_at (kernel_object.Notification notification) p' s
 2. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_obj notification = ActiveNtfn x3\<rbrakk> \<Longrightarrow> case ntfn_obj notification of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set epptr s \<and> (\<forall>p'. kheap s epptr = kheap s p' \<longrightarrow> epptr = p') | _ \<Rightarrow> none_is_waiting_ntfn epptr s
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = ActiveNtfn x3; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> none_is_waiting_ntfn epptr s
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = ActiveNtfn x3; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> ntfn_waiting_set epptr s = {}
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3 x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = ActiveNtfn x3; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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\<rbrakk> \<Longrightarrow> (x \<in> ntfn_waiting_set epptr s) = (x \<in> {})
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3 x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = ActiveNtfn x3; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x3 x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_obj notification = ActiveNtfn x3; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; \<forall>x. \<forall>xa\<in>state_hyp_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_hyp_refs_of s y; 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_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; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; \<forall>xa\<in>state_refs_of s x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> state_refs_of s y\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = None\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s
 2. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = Some a\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = None; 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_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; kheap s x = Some (TCB t); tcb_bound_notification t = Some epptr\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = Some a\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (3 subgoals):
 1. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = None; 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_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; kheap s x = Some (TCB t); tcb_bound_notification t = Some epptr\<rbrakk> \<Longrightarrow> (?y436 x t, ?tp436 x t) \<in> state_refs_of s x
 2. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = None; 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_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; kheap s x = Some (TCB t); tcb_bound_notification t = Some epptr; (x, symreftype (?tp436 x t)) \<in> state_refs_of s (?y436 x t)\<rbrakk> \<Longrightarrow> False
 3. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = Some a\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = None; 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_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; kheap s x = Some (TCB t); tcb_bound_notification t = Some epptr; (x, symreftype TCBBound) \<in> state_refs_of s epptr\<rbrakk> \<Longrightarrow> False
 2. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = Some a\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); valid_state s; ntfn_bound_tcb notification = Some a\<rbrakk> \<Longrightarrow> set_option (ntfn_bound_tcb notification) = ntfn_bound_set epptr s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; 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_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\<rbrakk> \<Longrightarrow> {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some epptr} proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; 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_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\<rbrakk> \<Longrightarrow> (?y474 a, ?tp474 a) \<in> state_refs_of s epptr
 2. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; 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_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; (epptr, symreftype (?tp474 a)) \<in> state_refs_of s (?y474 a)\<rbrakk> \<Longrightarrow> {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some epptr} proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; 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_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; (epptr, symreftype NTFNBound) \<in> state_refs_of s a\<rbrakk> \<Longrightarrow> {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some epptr} proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)\<rbrakk> \<Longrightarrow> {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some epptr} proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)\<rbrakk> \<Longrightarrow> (x \<in> {a}) = (x \<in> {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some epptr}) proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x)\<rbrakk> \<Longrightarrow> (x = a) = (\<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some epptr) proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); x = a\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some epptr
 2. \<And>a x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some epptr\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some epptr\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); kheap s x = Some (TCB t); tcb_bound_notification t = Some epptr\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); tcb_bound_notification t = Some epptr; ko_at (TCB t) x s\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t. \<lbrakk>kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; (epptr, TCBBound) \<in> (case kheap s a of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); tcb_bound_notification t = Some epptr; state_refs_of s x = refs_of (TCB t) \<and> (\<forall>(xa, tp)\<in>refs_of (TCB t). obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s)\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t x2. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; kheap s a = Some x2; (epptr, TCBBound) \<in> refs_of x2\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t x2. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; (epptr, TCBBound) \<in> refs_of x2; ko_at x2 a s\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t x2. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; (epptr, TCBBound) \<in> refs_of x2; state_refs_of s a = refs_of x2 \<and> (\<forall>(x, tp)\<in>refs_of x2. obj_at (\<lambda>ko. (a, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t x2 n. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some a; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; (epptr, TCBBound) \<in> refs_of x2; state_refs_of s a = refs_of x2 \<and> (\<forall>(x, tp)\<in>refs_of x2. obj_at (\<lambda>ko. (a, symreftype tp) \<in> refs_of ko) x s); a = word_of_nat n; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> x = a proof (prove)
goal (1 subgoal):
 1. \<And>a x t x2 n. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> refs_of ko); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some (word_of_nat n); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; (epptr, TCBBound) \<in> refs_of x2; state_refs_of s (word_of_nat n) = refs_of x2 \<and> (\<forall>x\<in>refs_of x2. case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (word_of_nat n, symreftype tp) \<in> refs_of ko) x s); a = word_of_nat n; n < 4294967296\<rbrakk> \<Longrightarrow> x = word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<And>x t x2 n. \<lbrakk>sym_refs (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some x \<Rightarrow> refs_of x); 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_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; tcb_bound_notification t = Some epptr; kheap s epptr = Some (kernel_object.Notification notification); ntfn_bound_tcb notification = Some (word_of_nat n); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; state_refs_of s x = insert (epptr, TCBBound) (tcb_st_refs_of (tcb_state t)); obj_at (\<lambda>ko. (x, NTFNBound) \<in> refs_of ko) epptr s; \<forall>xa\<in>tcb_st_refs_of (tcb_state t). case xa of (xa, tp) \<Rightarrow> obj_at (\<lambda>ko. (x, symreftype tp) \<in> refs_of ko) xa s; (epptr, TCBBound) \<in> refs_of x2; n < 4294967296; state_refs_of s (word_of_nat n) = refs_of x2; \<forall>x\<in>refs_of x2. case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (word_of_nat n, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> x = word_of_nat n proof (prove)
goal:
No subgoals!