theory IpcCancel_R

lemma cancelAllSignals_corres:
  "corres dc (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn)
             (cancel_all_signals ntfn) (cancelAllSignals ntfn)" apply (simp add: cancel_all_signals_def cancelAllSignals_def) apply (rule corres_underlying_split [OF _ _ get_simple_ko_sp get_ntfn_sp']) apply (rule corres_guard_imp [OF getNotification_corres]) apply simp+ apply (case_tac "ntfn_obj ntfna", simp_all add: ntfn_relation_def) apply (rule corres_guard_imp) apply (rule corres_split[OF setNotification_corres]) apply (simp add: ntfn_relation_def) apply (rule corres_split[OF _ rescheduleRequired_corres]) apply (rule ep_cancel_corres_helper) apply (wp mapM_x_wp'[where 'b="det_ext state"]
                 weak_sch_act_wf_lift_linear setThreadState_not_st
                 set_thread_state_runnable_weak_valid_sched_action
            | simp)+ apply (rename_tac list) apply (rule_tac R="\<lambda>_ s. (\<forall>x\<in>set list. tcb_at' x s) \<and> valid_objs' s"
                   in hoare_post_add) apply (rule mapM_x_wp') apply (rule hoare_name_pre_state) apply (wpsimp wp: hoare_vcg_const_Ball_lift
                        sts_st_tcb' sts_valid_queues setThreadState_not_st
                  simp: valid_tcb_state'_def) apply (wp hoare_vcg_const_Ball_lift set_ntfn_aligned' set_ntfn_valid_objs'
               weak_sch_act_wf_lift_linear
          | simp)+ apply (clarsimp simp: invs'_def valid_state'_def invs_valid_pspace valid_obj_def valid_ntfn_def invs_weak_sch_act_wf valid_ntfn'_def valid_pspace'_def
              valid_sched_def valid_sched_action_def valid_obj'_def projectKOs | erule obj_at_valid_objsE | drule ko_at_valid_objs')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn) (cancel_all_signals ntfn) (cancelAllSignals ntfn) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn) (do ntfna <- get_notification ntfn;
case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfn $ ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od) (do ntfna <- getNotification ntfn;
case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od) proof (prove)
goal (2 subgoals):
 1. corres ?r' (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn) (get_notification ntfn) (getNotification ntfn)
 2. \<And>ntfna ntfnaa. ?r' ntfna ntfnaa \<Longrightarrow> corres dc (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) (case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfn $ ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()) (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s. (invs and valid_sched and ntfn_at ntfn) s \<Longrightarrow> ntfn_at ntfn s
 2. \<And>s. (invs' and ntfn_at' ntfn) s \<Longrightarrow> ntfn_at' ntfn s
 3. \<And>ntfna ntfnaa. ntfn_relation ntfna ntfnaa \<Longrightarrow> corres dc (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) (case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfn $ ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()) (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna ntfnaa. ntfn_relation ntfna ntfnaa \<Longrightarrow> corres dc (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) (case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfn $ ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()) (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) (do _ <- set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od) (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2;
rescheduleRequired
od) proof (prove)
goal (3 subgoals):
 1. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?Q12 ntfna ntfnaa x2) (?Q'12 ntfna ntfnaa x2) (do _ <- set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn);
y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od) (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2;
rescheduleRequired
od)
 2. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> ?Q12 ntfna ntfnaa x2 s
 3. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> ?Q'12 ntfna ntfnaa x2 s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn ntfna x2. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna)
 2. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> corres dc (?R16 ntfn ntfna x2 uu_) (?R'16 ntfn ntfna x2 y) (do y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od) (do y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2;
rescheduleRequired
od)
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>?R16 ntfna ntfnaa x2\<rbrace>
 4. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>?R'16 ntfna ntfnaa x2\<rbrace>
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 6. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> corres dc (?R16 ntfn ntfna x2 uu_) (?R'16 ntfn ntfna x2 y) (do y <- mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2;
reschedule_required
od) (do y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2;
rescheduleRequired
od)
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>?R16 ntfna ntfnaa x2\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>?R'16 ntfna ntfnaa x2\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> corres (?r'22 ntfn ntfna x2 uu_ y) (?P24 ntfn ntfna x2 uu_) (?P'26 ntfn ntfna x2 y) (mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2) (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2)
 2. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 ntfn ntfna x2 uu_\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2 \<lbrace>\<lambda>y. weak_valid_sched_action and valid_etcbs\<rbrace>
 3. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ntfn ntfna x2 y\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2 \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 4. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>uu_. ?P24 ntfna ntfnaa x2 uu_ and ?Q25 ntfna ntfnaa x2 uu_\<rbrace>
 5. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. ?P'26 ntfna ntfnaa x2 y and ?Q'27 ntfna ntfnaa x2 y\<rbrace>
 6. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 7. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 ntfn ntfna x2 uu_\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) x2 \<lbrace>\<lambda>y. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>ntfn ntfna x2 uu_ y. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2; dc uu_ y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ntfn ntfna x2 y\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2 \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>uu_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and ?Q25 ntfna ntfnaa x2 uu_\<rbrace>
 4. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'27 ntfna ntfnaa x2 y\<rbrace>
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 6. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna x2. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ntfn ntfna x2 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x2 \<lbrace>\<lambda>y s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'27 ntfna ntfnaa x2 y\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna list. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ntfn ntfna list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>y s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'27 ntfna ntfnaa x2 y\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna list. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list\<rbrakk> \<Longrightarrow> \<lbrace>?Q'27 ntfn ntfna list ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list \<lbrace>\<lambda>r s. ((\<forall>x\<in>set list. tcb_at' x s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and ?Q'27 ntfna ntfnaa x2 y\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna list x. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; x \<in> set list\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. ((\<forall>x\<in>set list. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r a. ((\<forall>x\<in>set list. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. ((\<forall>x\<in>set x2. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna list x s. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; x \<in> set list; ((\<forall>x\<in>set list. tcb_at' x s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r a. ((\<forall>x\<in>set list. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 3. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. ((\<forall>x\<in>set x2. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace>
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 5. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (4 subgoals):
 1. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 ntfna ntfnaa x2\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>_. (\<lambda>s. \<forall>t\<in>set x2. tcb_at t s) and valid_etcbs and (weak_valid_sched_action and valid_etcbs)\<rbrace>
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 ntfna ntfnaa x2\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>y. (\<lambda>s. \<forall>t\<in>set x2. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs' and (\<lambda>a. ((\<forall>x\<in>set x2. tcb_at' x a) \<and> valid_objs' a) \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)\<rbrace>
 3. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (invs and valid_sched and ntfn_at ntfn)) s\<rbrakk> \<Longrightarrow> (ntfn_at ntfn and ?Q16 ntfna ntfnaa x2) s
 4. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and ?Q'16 ntfna ntfnaa x2) s proof (prove)
goal (2 subgoals):
 1. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; ko_at (Notification ntfna) ntfn s \<and> invs s \<and> valid_sched s \<and> ntfn_at ntfn s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x2. tcb_at x s) \<and> valid_etcbs s \<and> weak_valid_sched_action s \<and> valid_etcbs s
 2. \<And>ntfna ntfnaa x2 s. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2; (invs' and ntfn_at' ntfn and ko_at' ntfnaa ntfn) s\<rbrakk> \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> (valid_objs' and valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa)) s \<and> (\<forall>x\<in>set x2. tcb_at' x s) \<and> (valid_objs' and valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa)) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s proof (prove)
goal:
No subgoals!