theory Ipc_IF

lemma send_signal_globals_equiv:
  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs
                    and sym_refs \<circ> state_refs_of and pspace_distinct and valid_idle\<rbrace>
   send_signal ntfnptr badge
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding send_signal_def apply (wp set_notification_globals_equiv possible_switch_to_globals_equiv
            set_thread_state_globals_equiv as_user_globals_equiv cancel_ipc_blocked_globals_equiv
            update_waiting_ntfn_globals_equiv get_simple_ko_wp gts_wp
         | wpc | simp)+ apply clarsimp apply (frule (1) sym_refs_ko_atD) apply (intro allI impI conjI) prefer 4 apply clarsimp apply (frule_tac t="idle_thread sa" and P="\<lambda>ref. \<not> idle ref" in ntfn_queued_st_tcb_at') by (auto simp: pred_tcb_at_def obj_at_def valid_idle_def receive_blocked_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and sym_refs \<circ> state_refs_of and pspace_distinct and valid_idle\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and sym_refs \<circ> state_refs_of and pspace_distinct and valid_idle\<rbrace> do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> valid_objs sa \<and> valid_arch_state sa \<and> valid_global_refs sa \<and> sym_refs (state_refs_of sa) \<and> pspace_distinct sa \<and> valid_idle sa \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr sa \<longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x sa \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x sa \<and> x \<noteq> idle_thread sa))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa \<and> idle_thread sa \<notin> set x \<and> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x) proof (prove)
goal (1 subgoal):
 1. \<And>sa ntfn. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa\<rbrakk> \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x sa \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x sa \<and> x \<noteq> idle_thread sa))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa \<and> idle_thread sa \<notin> set x \<and> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x) proof (prove)
goal (1 subgoal):
 1. \<And>sa ntfn. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa)\<rbrakk> \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x sa \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x sa \<and> x \<noteq> idle_thread sa))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa \<and> idle_thread sa \<notin> set x \<and> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x) proof (prove)
goal (5 subgoals):
 1. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x sa
 2. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa
 3. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa
 4. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> idle_thread sa \<notin> set x
 5. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x proof (prove)
goal (5 subgoals):
 1. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> idle_thread sa \<notin> set x
 2. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x sa
 3. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa
 4. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa
 5. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x proof (prove)
goal (5 subgoals):
 1. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x\<rbrakk> \<Longrightarrow> False
 2. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x sa
 3. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa
 4. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa
 5. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x proof (prove)
goal (9 subgoals):
 1. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x\<rbrakk> \<Longrightarrow> (idle_thread sa, ?rt117 sa ntfn x) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x\<rbrakk> \<Longrightarrow> valid_objs sa
 3. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of sa)
 4. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x\<rbrakk> \<Longrightarrow> BlockedOnNotification ntfnptr \<noteq> IdleThreadState
 5. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = WaitingNtfn x; state_refs_of sa ntfnptr = set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa; idle_thread sa \<in> set x; st_tcb_at (\<lambda>ref. ref \<noteq> IdleThreadState) (idle_thread sa) sa\<rbrakk> \<Longrightarrow> False
 6. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x sa
 7. \<And>sa ntfn x st. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x sa; receive_blocked st\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread sa
 8. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ko_at (Notification (?ntfn78 ntfn x)) ntfnptr sa
 9. \<And>sa ntfn x. \<lbrakk>globals_equiv s sa; valid_objs sa; valid_arch_state sa; valid_global_refs sa; sym_refs (state_refs_of sa); pspace_distinct sa; valid_idle sa; ko_at (Notification ntfn) ntfnptr sa; state_refs_of sa ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x sa); ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn78 ntfn x) = WaitingNtfn x