theory IpcCancel_AI

lemma cancel_all_signals_invs:
  "\<lbrace>invs\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: cancel_all_signals_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp cancel_all_invs_helper set_simple_ko_valid_objs valid_irq_node_typ
             hoare_vcg_const_Ball_lift valid_ioports_lift
        | wpc
        | simp add: live_def)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def) apply (rule conjI) apply (fastforce simp: valid_obj_def valid_ntfn_def elim!: obj_at_valid_objsE) apply (rule conjI) apply (fastforce simp: live_def elim!: if_live_then_nonz_capD) apply (rule conjI) apply (fastforce simp: is_ntfn elim!: ko_at_weakenE) apply (rule conjI) apply (fastforce simp: st_tcb_at_refs_of_rev
                    dest: bspec sym_refs_ko_atD
                    elim: st_tcb_ex_cap) apply (rule conjI[rotated]) apply (fastforce elim!: ntfn_queued_st_tcb_at) apply (rule delta_sym_refs, assumption) apply (fastforce dest!: refs_in_ntfn_bound_refs ko_at_state_refs_ofD
                    split: if_split_asm) apply (clarsimp split:if_split_asm) apply (fastforce dest: waiting_ntfn_list_tcb_at refs_in_ntfn_bound_refs
                     simp: obj_at_def is_tcb_def) apply (rule conjI) apply (fastforce dest: refs_in_ntfn_bound_refs symreftype_inverse') apply (frule (2) waiting_ntfn_list_tcb_at) apply (fastforce simp: st_tcb_at_refs_of_rev refs_in_tcb_bound_refs
                    dest: bspec sym_refs_ko_atD st_tcb_at_state_refs_ofD) apply (fastforce simp: ntfn_bound_refs_def valid_obj_def valid_ntfn_def refs_of_rev
                  dest!: symreftype_inverse' ko_at_state_refs_ofD
                  split: option.splits
                  elim!: obj_at_valid_objsE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and invs\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and invs) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at (Notification ntfn) ntfnptr s \<and> invs s \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> valid_objs s \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> zombies_final s \<and> valid_mdb s \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> sym_refs (state_hyp_refs_of s) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x. ex_nonz_cap_to x s) \<and> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. ex_nonz_cap_to x s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) \<and> (\<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x. st_tcb_at (\<lambda>a. \<not> halted a \<and> a \<noteq> BlockedOnReply) x s
 2. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>xa. if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> (if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y \<in> set x then {r \<in> if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y. snd r = TCBBound} else if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y \<in> set x then {r \<in> if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y. snd r = TCBBound} else if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa \<in> set x then {r \<in> if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa. snd r = TCBBound} else if xa = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y \<in> set x then {r \<in> if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y. snd r = TCBBound} else if y = ntfnptr then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<in> set x; (y, tp) \<in> ntfn_bound_refs (ntfn_bound_tcb ntfn) \<longrightarrow> tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<in> ntfn_bound_refs (ntfn_bound_tcb ntfn) \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> ntfn_bound_refs (ntfn_bound_tcb ntfn) \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (ntfnptr \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn))) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> state_refs_of s y))
 3. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> ntfn_bound_refs (ntfn_bound_tcb ntfn) \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (ntfnptr \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn))) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> y = ntfnptr \<longrightarrow> (ntfnptr \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> ntfn_bound_refs (ntfn_bound_tcb ntfn) \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (ntfnptr \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn))
 2. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> state_refs_of s y)
 3. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x xa y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s xa; xa \<in> set x; xa \<noteq> ntfnptr; tp \<noteq> TCBBound; \<forall>t\<in>set x. tcb_at t s\<rbrakk> \<Longrightarrow> y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (xa, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (xa, symreftype tp) \<notin> state_refs_of s y)
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ntfn_obj ntfn = WaitingNtfn x; (y, tp) \<in> state_refs_of s ntfnptr; ntfnptr \<notin> set x; (y, tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)\<rbrakk> \<Longrightarrow> (y = ntfnptr \<longrightarrow> (ntfnptr, symreftype tp) \<notin> ntfn_bound_refs (ntfn_bound_tcb ntfn)) \<and> (y \<noteq> ntfnptr \<longrightarrow> (y \<in> set x \<longrightarrow> (ntfnptr, symreftype tp) \<in> state_refs_of s y \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<notin> set x \<longrightarrow> (ntfnptr, symreftype tp) \<notin> state_refs_of s y)) proof (prove)
goal:
No subgoals!