theory KHeap_DR

lemma fast_finalise_wait_ntfn:
  "dcorres dc \<top>
     (valid_state and valid_idle and valid_etcbs
      and ko_at (kernel_object.Notification ntfn) epptr
      and (\<lambda>_. ntfn_obj ntfn = (Structures_A.ntfn.WaitingNtfn list)))
     (PageTableUnmap_D.cancel_all_ipc epptr)
     (do _ \<leftarrow> set_notification epptr $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn;
         _ \<leftarrow> mapM_x (\<lambda>t. do _ \<leftarrow> set_thread_state t Structures_A.thread_state.Restart;
                             tcb_sched_action tcb_sched_enqueue t
                          od) list;
         reschedule_required
      od)" supply if_cong[cong] option.case_cong[cong] apply (simp add:cancel_all_ipc_def_alt1) apply (rule dcorres_absorb_get_l) apply clarsimp apply (rule corres_dummy_return_pl) apply (rule corres_split_forwards'[where r'=dc and Q="\<lambda>_. \<top>", OF _ _ set_ntfn_exec_wp]) apply (rule corres_dummy_set_notification[THEN corres_guard_imp],simp+) apply (rule_tac Q'=
    "\<lambda>s. (\<forall>x\<in> (set list). tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s')"
    in corres_guard_imp[where Q=\<top>]) apply (rule dcorres_rhs_noop_below_True[OF reschedule_required_dcorres]) apply (rule_tac lift_func = id in set_list_modify_corres_helper) apply (clarsimp simp:obj_at_def) apply (drule valid_objs_valid_ntfn_simp[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply (simp add:valid_ntfn_def) apply (simp add:inj_on_def) apply (clarsimp simp:obj_at_def) apply (frule_tac epptr=epptr in get_notification_pick) apply (simp add:valid_ntfn_abstract_def)+ apply (subst is_thread_blocked_on_sth[simplified]) apply (clarsimp simp:ntfn_waiting_set_lift ep_waiting_set_send_lift ep_waiting_set_recv_lift) apply (frule ntfn_not_waiting_ep_recv[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply (drule ntfn_not_waiting_ep_send[rotated]) apply (simp add:valid_state_def valid_pspace_def) apply clarsimp apply (clarsimp simp:set_thread_state_def tcb_filter_modify_def bind_assoc) apply (rule dcorres_absorb_gets_the) apply (rule dcorres_rhs_noop_below_True[OF dcorres_rhs_noop_below_True[OF tcb_sched_action_dcorres _], OF set_thread_state_ext_dcorres _]) apply (clarsimp simp: set_object_def get_object_def in_monad simpler_modify_def put_def
                           return_def get_def bind_def corres_underlying_def select_f_def mk_ef_def) apply (frule ntfn_not_idle) apply (fastforce simp: obj_at_def is_ntfn_def) apply (clarsimp dest!:get_tcb_SomeD split:if_splits) apply (drule get_tcb_rev)+ apply (clarsimp simp:transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp dest!: get_tcb_SomeD simp:transform_objects_update_other split:if_splits option.splits) apply (drule get_tcb_rev)+ apply (clarsimp simp:obj_at_def) apply (frule_tac epptr = epptr in get_notification_pick,simp,clarsimp simp:valid_ntfn_abstract_def) apply (clarsimp split:option.splits simp:lift_simp not_idle_thread_def transform_tcb_def) apply (fastforce simp: remove_pending_operation_def transform_tcb_def infer_tcb_pending_op_def restrict_map_def infer_tcb_bound_notification_def tcb_slots
                            map_add_def is_tcb get_tcb_def is_etcb_at_def split: option.splits
                      cong: transform_full_intent_cong) apply (clarsimp simp:not_idle_thread_def | wp)+ apply (frule_tac a = "idle_thread s" in   pending_thread_in_wait_not_idle) apply (simp add:not_idle_thread_def)+ apply (frule ntfn_not_idle) apply (fastforce simp:obj_at_def is_ntfn_def) apply (clarsimp simp:valid_idle_def st_tcb_at_def obj_at_def ep_not_idle not_idle_thread_def) apply (drule_tac epptr=epptr in get_notification_pick) apply (simp) apply (clarsimp simp:valid_ntfn_abstract_def ntfn_waiting_set_def) apply (drule_tac ptr=x in valid_etcbs_tcb_etcb) apply (auto simp: is_etcb_at_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs and ko_at (kernel_object.Notification ntfn) epptr and (\<lambda>_. ntfn_obj ntfn = WaitingNtfn list)) (PageTableUnmap_D.cancel_all_ipc epptr) (do _ <- set_notification epptr $ ntfn_set_obj ntfn IdleNtfn;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs and ko_at (kernel_object.Notification ntfn) epptr and (\<lambda>_. ntfn_obj ntfn = WaitingNtfn list)) (PageTableUnmap_D.cancel_all_ipc epptr) (do _ <- set_notification epptr $ ntfn_set_obj ntfn IdleNtfn;
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_state and valid_idle and valid_etcbs and ko_at (kernel_object.Notification ntfn) epptr and (\<lambda>_. ntfn_obj ntfn = WaitingNtfn list)) (do s <- get;
tcb_filter_modify {x. \<exists>tcb. cdl_objects s x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (\<lambda>x. case x of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))
od) (do _ <- set_notification epptr (ntfn_set_obj ntfn IdleNtfn);
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_state and valid_idle and valid_etcbs and ko_at (kernel_object.Notification ntfn) epptr and (\<lambda>_. ntfn_obj ntfn = WaitingNtfn list)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (\<lambda>x. case x of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) (do _ <- set_notification epptr (ntfn_set_obj ntfn IdleNtfn);
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_notification epptr (ntfn_set_obj ntfn IdleNtfn);
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do return (?b6 s');
tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))
od) (do _ <- set_notification epptr (ntfn_set_obj ntfn IdleNtfn);
_ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return (?b6 s')) (set_notification epptr (ntfn_set_obj ntfn IdleNtfn))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return (?b6 s') \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s' rv uu_. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; dc rv uu_\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s'a. s'a = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') (K_bind (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) rv) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s'a. s'a = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list;
reschedule_required
od)
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (mapM_x (\<lambda>t. do _ <- set_thread_state t Restart;
tcb_sched_action tcb_sched_enqueue t
od) list)
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (8 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; valid_ntfn ntfn s'\<rbrakk> \<Longrightarrow> distinct list
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> inj_on id (set list)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 6. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 8. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; valid_ntfn ntfn s'\<rbrakk> \<Longrightarrow> distinct list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> inj_on id (set list)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 5. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> inj_on id (set list)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = id ` set list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = set list
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> valid_state s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; valid_ntfn_abstract ntfn epptr s'\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = set list
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s' \<and> list \<noteq> [] \<and> set list = ntfn_waiting_set epptr s' \<and> (\<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p')\<rbrakk> \<Longrightarrow> {x. \<exists>tcb. cdl_objects (transform s') x = Some (Tcb tcb) \<and> is_thread_blocked_on_endpoint tcb epptr} = ntfn_waiting_set epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s' \<and> list \<noteq> [] \<and> set list = ntfn_waiting_set epptr s' \<and> (\<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p')\<rbrakk> \<Longrightarrow> get_waiting_sync_recv_threads epptr (transform s') \<union> get_waiting_sync_send_threads epptr (transform s') \<union> get_waiting_ntfn_recv_threads epptr (transform s') = ntfn_waiting_set epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ep_waiting_set_send epptr s' \<union> ntfn_waiting_set epptr s' = ntfn_waiting_set epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; ep_waiting_set_recv epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ep_waiting_set_send epptr s' \<union> ntfn_waiting_set epptr s' = ntfn_waiting_set epptr s'
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; ep_waiting_set_recv epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ep_waiting_set_send epptr s' \<union> ntfn_waiting_set epptr s' = ntfn_waiting_set epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; ep_waiting_set_recv epptr s' = {}\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; ep_waiting_set_recv epptr s' = {}; ep_waiting_set_send epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ep_waiting_set_send epptr s' \<union> ntfn_waiting_set epptr s' = ntfn_waiting_set epptr s'
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 4. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; ep_waiting_set_recv epptr s' = {}; ep_waiting_set_send epptr s' = {}\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s' \<union> ep_waiting_set_send epptr s' \<union> ntfn_waiting_set epptr s' = ntfn_waiting_set epptr s'
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>a\<in>set list. dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (tcb_filter_modify {id a} (case_option undefined (case_cdl_object undefined undefined (\<lambda>tcb. Some (Tcb (remove_pending_operation tcb RestartCap))) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) (\<lambda>a. undefined) undefined (\<lambda>a. undefined)))) (do _ <- set_thread_state a Restart;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. tcb_at a s \<and> is_etcb_at a s \<and> not_idle_thread a s \<and> valid_idle s \<and> idle_thread s = idle_thread s') (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (do x <- gets_the (get_tcb a);
x <- KHeap_A.set_object a (TCB (update_tcb_state Restart x));
_ <- set_thread_state_ext a;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a \<and> is_etcb_at a s'a \<and> not_idle_thread a s'a \<and> valid_idle s'a \<and> idle_thread s'a = idle_thread s'; get_tcb a s'a = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (do x <- KHeap_A.set_object a (TCB (update_tcb_state Restart obj'));
_ <- set_thread_state_ext a;
tcb_sched_action tcb_sched_enqueue a
od)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a \<and> is_etcb_at a s'a \<and> not_idle_thread a s'a \<and> valid_idle s'a \<and> idle_thread s'a = idle_thread s'; get_tcb a s'a = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects s a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects s x\<rparr>)) (KHeap_A.set_object a (TCB (update_tcb_state Restart obj')))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; get_tcb a s'a = Some obj'; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (5 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; get_tcb a s'a = Some obj'; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ntfn_at (?epptr76 s' a s'a obj' tcb) s'
 2. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; get_tcb a s'a = Some obj'; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; kheap s'a a = Some (TCB tcb); not_idle_thread (?epptr76 s' a s'a obj' tcb) s'\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 3. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a obj' tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; get_tcb a s'a = Some obj'; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; kheap s'a a = Some (TCB tcb); not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart obj'))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) = transform s'a\<lparr>cdl_objects := \<lambda>x. if x = a then case cdl_objects (transform s'a) a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else cdl_objects (transform s'a) x\<rparr>
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) = (\<lambda>x. if x = a then case transform_objects s'a a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else transform_objects s'a x)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) x = (if x = a then case transform_objects s'a a of Some (Tcb tcb) \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)) else transform_objects s'a x)
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; kheap s'a a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; tcb_at a s'a; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; a \<in> set list; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb; kheap s'a a = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; a \<in> ntfn_waiting_set epptr s'; is_etcb_at a s'a; not_idle_thread a s'a; valid_idle s'a; idle_thread s'a = idle_thread s'; not_idle_thread epptr s'; get_tcb a s'a = Some tcb; kheap s'a a = Some ko; is_tcb ko; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> (transform_objects s'a a = None \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = undefined) \<and> (\<forall>x2. transform_objects s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> transform_objects (update_kheap ((kheap s'a)(a \<mapsto> TCB (update_tcb_state Restart tcb))) s'a) a = (case x2 of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (4 subgoals):
 1. \<And>s' a s'a tcb x ko. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; a \<in> ntfn_waiting_set epptr s'; is_etcb_at a s'a; a \<noteq> idle_thread s'; valid_idle s'a; idle_thread s'a = idle_thread s'; epptr \<noteq> idle_thread s'; get_tcb a s'a = Some tcb; kheap s'a a = Some ko; is_tcb ko; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = ntfn_waiting_set epptr s'; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> (ekheap s'a a = None \<longrightarrow> x = a \<longrightarrow> Some undefined = (case transform_object (machine_state s'a) a None ko of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap)))) \<and> (\<forall>x2. ekheap s'a a = Some x2 \<longrightarrow> x = a \<longrightarrow> Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> RestartCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s'a) a tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain x2\<rparr>) = (case transform_object (machine_state s'a) a (Some x2) ko of Tcb tcb \<Rightarrow> Some (Tcb (remove_pending_operation tcb RestartCap))))
 2. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. \<forall>y\<in>set list. x \<noteq> y \<longrightarrow> \<lbrace>\<lambda>s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace> do _ <- set_thread_state x Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv s. tcb_at y s \<and> is_etcb_at y s \<and> not_idle_thread y s \<and> valid_idle s \<and> idle_thread s = idle_thread s'\<rbrace>
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (3 subgoals):
 1. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (7 subgoals):
 1. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> valid_idle s'
 2. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> idle_thread s \<in> set (?list190 s' y s)
 3. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification (?ntfn190 s' y s)) (?epptr190 s' y s) s'
 4. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> ntfn_obj (?ntfn190 s' y s) = WaitingNtfn (?list190 s' y s)
 5. \<And>s' y s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; idle_thread s' \<in> set list; y \<in> set list; tcb_at y s; is_etcb_at y s; y \<noteq> idle_thread s'; valid_idle s; idle_thread s = idle_thread s'; not_idle_thread (idle_thread s) s'\<rbrakk> \<Longrightarrow> False
 6. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; True\<rbrakk> \<Longrightarrow> True
 7. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x s \<and> is_etcb_at x s \<and> not_idle_thread x s \<and> valid_idle s \<and> idle_thread s = idle_thread s' proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread s' \<and> valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'\<rbrakk> \<Longrightarrow> ntfn_at (?epptr192 s' s) s'
 2. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'; not_idle_thread (?epptr192 s' s) s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread s' \<and> valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>valid_state s'; valid_idle s'; valid_etcbs s'; ko_at (kernel_object.Notification ntfn) epptr s'; ntfn_obj ntfn = WaitingNtfn list; s = update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s'; not_idle_thread epptr s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>set list. tcb_at x (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread s' \<and> valid_idle (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s') proof (prove)
goal (1 subgoal):
 1. \<And>s' x. \<lbrakk>valid_state s'; valid_etcbs s'; kheap s' epptr = Some (kernel_object.Notification ntfn); ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) \<and> is_etcb_at epptr s' \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread_ptr \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' x. \<lbrakk>valid_state s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr\<rbrakk> \<Longrightarrow> valid_state s'
 2. \<And>s' x. \<lbrakk>valid_state s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; valid_ntfn_abstract ntfn epptr s'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) \<and> is_etcb_at epptr s' \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread_ptr \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) proof (prove)
goal (1 subgoal):
 1. \<And>s' x. \<lbrakk>valid_state s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; x \<in> set list; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; valid_ntfn_abstract ntfn epptr s'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) \<and> is_etcb_at epptr s' \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) \<and> (x \<noteq> epptr \<longrightarrow> (\<exists>ko. kheap s' x = Some ko \<and> is_tcb ko) \<and> is_etcb_at x s' \<and> x \<noteq> idle_thread_ptr \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) proof (prove)
goal (1 subgoal):
 1. \<And>s' x t. \<lbrakk>valid_state s'; valid_etcbs s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; kheap s' epptr = Some (kernel_object.Notification ntfn); kheap s' x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr}; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) \<and> is_etcb_at epptr s' \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) \<and> (x \<noteq> epptr \<longrightarrow> is_etcb_at x s' \<and> x \<noteq> idle_thread_ptr \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) proof (prove)
goal (2 subgoals):
 1. \<And>s' x t. \<lbrakk>valid_state s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; kheap s' epptr = Some (kernel_object.Notification ntfn); kheap s' x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr}; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'\<rbrakk> \<Longrightarrow> kheap s' x = Some (TCB (?tcb218 s' x t))
 2. \<And>s' x t. \<lbrakk>valid_state s'; ntfn_obj ntfn = WaitingNtfn list; epptr \<noteq> idle_thread_ptr; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; kheap s' epptr = Some (kernel_object.Notification ntfn); kheap s' x = Some (TCB t); tcb_state t = BlockedOnNotification epptr; set_option (ntfn_bound_tcb ntfn) = ntfn_bound_set epptr s'; list \<noteq> []; set list = {tcb. \<exists>t. kheap s' tcb = Some (TCB t) \<and> tcb_state t = BlockedOnNotification epptr}; \<forall>p'. Some (kernel_object.Notification ntfn) = kheap s' p' \<longrightarrow> epptr = p'; \<exists>etcb. ekheap s' x = Some etcb\<rbrakk> \<Longrightarrow> (x = epptr \<longrightarrow> is_tcb (kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn)) \<and> is_etcb_at epptr s' \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) \<and> (x \<noteq> epptr \<longrightarrow> is_etcb_at x s' \<and> x \<noteq> idle_thread_ptr \<and> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr (update_kheap ((kheap s')(epptr \<mapsto> kernel_object.Notification (ntfn_set_obj ntfn IdleNtfn))) s')) proof (prove)
goal:
No subgoals!