theory Finalise_IF

lemma ntfn_queues_are_invisible_or_ntfns_are_equal':
  "\<lbrakk> (pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag;
     ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s';
     reads_equiv aag s s'; affects_equiv aag l s s';
     valid_objs s; sym_refs (state_refs_of s); valid_objs s';
     sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s' \<rbrakk>
     \<Longrightarrow> \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn) \<longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn'" apply (rule impI) apply (case_tac "\<exists>list. ntfn_obj ntfn = WaitingNtfn list") apply (erule exE) apply (drule (1) not_ntfn_queue_invisible) apply clarsimp apply (erule disjE) apply (drule_tac auth="Receive" and t="pasObjectAbs aag t" in reads_read_queued_thread_read_ep) apply blast apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (drule_tac P="receive_blocked_on ntfnptr" and s=s and t=t in ntfn_queued_st_tcb_at') apply (simp)+ apply (simp add: thread_st_auth_def split: option.splits) apply (clarsimp simp: tcb_states_of_state_def st_tcb_def2 receive_blocked_on_tcb_st_to_auth) apply blast apply assumption apply (fastforce dest: reads_affects_equiv_kheap_eq simp: obj_at_def) apply (drule_tac auth="Receive" and t="pasObjectAbs aag t" in reads_read_queued_thread_read_ep) apply blast apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (drule_tac P="receive_blocked_on ntfnptr" and s=s and t=t in ntfn_queued_st_tcb_at') apply (simp)+ apply (simp add: thread_st_auth_def split: option.splits) apply (clarsimp simp: tcb_states_of_state_def st_tcb_def2 receive_blocked_on_tcb_st_to_auth) apply blast apply (erule conjE, assumption) apply (drule_tac x=ntfnptr in reads_affects_equiv_kheap_eq, simp+) apply (fastforce simp: obj_at_def) apply (case_tac "ntfn_obj ntfn", auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn) \<longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn)\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<exists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; \<exists>t\<in>set list. aag_can_read aag t \<or> aag_can_affect aag l t\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t \<or> aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (3 subgoals):
 1. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (7 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Reset \<in> {Notify, SyncSend, Reset}
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 5. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 7. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> (t, Receive, ntfnptr) \<in> state_objs_to_policy s
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (10 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> (t, ?rt29 list t) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 5. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 6. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 7. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 8. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 9. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 10. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (\<exists>y. tcb_states_of_state s t = Some y) \<and> (\<forall>x2. tcb_states_of_state s t = Some x2 \<longrightarrow> (ntfnptr, Receive) \<in> tcb_st_to_auth x2)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 4. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (4 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l14 list t)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l14 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 3. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 4. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (3 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_read aag t; aag_can_read aag ntfnptr\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list t. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (6 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Reset \<in> {Notify, SyncSend, Reset}
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 5. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 6. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> (t, Receive, ntfnptr) \<in> state_objs_to_policy s
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (9 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> (t, ?rt70 list t) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 5. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 6. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 7. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 8. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 9. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (ntfnptr, Receive) \<in> thread_st_auth s t
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (5 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; st_tcb_at (receive_blocked_on ntfnptr) t s\<rbrakk> \<Longrightarrow> (\<exists>y. tcb_states_of_state s t = Some y) \<and> (\<forall>x2. tcb_states_of_state s t = Some x2 \<longrightarrow> (ntfnptr, Receive) \<in> tcb_st_to_auth x2)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 4. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 5. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (4 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 3. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 4. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (3 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> subjectReads (pasPolicy aag) (?l55 list t)
 2. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) (?l55 list t)\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (2 subgoals):
 1. \<And>list t. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; ntfn_obj ntfn = WaitingNtfn list; t \<in> set list; aag_can_affect aag l t; pasObjectAbs aag ntfnptr \<in> subjectReads (pasPolicy aag) l; kheap s ntfnptr = kheap s' ntfnptr\<rbrakk> \<Longrightarrow> WaitingNtfn list = ntfn_obj ntfn'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ko_at (Notification ntfn') ntfnptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ntfn_queue_invisible aag l (ntfn_obj ntfn); \<nexists>list. ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> ntfn_obj ntfn = ntfn_obj ntfn' proof (prove)
goal:
No subgoals!