theory Ipc_R

lemma sai_invs'[wp]:
  "\<lbrace>invs' and ex_nonz_cap_to' ntfnptr\<rbrace>
     sendSignal ntfnptr badge \<lbrace>\<lambda>y. invs'\<rbrace>" unfolding sendSignal_def including no_pre apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (case_tac "ntfnObj nTFN", simp_all) prefer 3 apply (rename_tac list) apply (case_tac list,
           simp_all split del: if_split
                          add: setMessageInfo_def)[1] apply (rule hoare_pre) apply (wp hoare_convert_imp [OF asUser_nosch]
               hoare_convert_imp [OF setMRs_sch_act])+ apply (clarsimp simp:conj_comms) apply (simp add: invs'_def valid_state'_def) apply ((wp valid_irq_node_lift sts_valid_objs' setThreadState_ct_not_inQ
               sts_valid_queues [where st="Structures_H.thread_state.Running", simplified]
               set_ntfn_valid_objs' cur_tcb_lift sts_st_tcb'
               hoare_convert_imp [OF setNotification_nosch]
           | simp split del: if_split)+)[3] apply (intro conjI[rotated];
      (solves \<open>clarsimp simp: invs'_def valid_state'_def valid_pspace'_def\<close>)?) apply clarsimp apply (clarsimp simp: invs'_def valid_state'_def split del: if_split) apply (drule(1) ct_not_in_ntfnQueue, simp+) apply clarsimp apply (frule ko_at_valid_objs', clarsimp) apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def
                         split: list.splits) apply (clarsimp simp: invs'_def valid_state'_def) apply (clarsimp simp: st_tcb_at_refs_of_rev' valid_idle'_def pred_tcb_at'_def idle_tcb'_def
                        dest!: sym_refs_ko_atD' sym_refs_st_tcb_atD' sym_refs_obj_atD'
                        split: list.splits) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) apply (frule(1) ko_at_valid_objs') apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def
                    split: list.splits option.splits) apply (clarsimp elim!: if_live_then_nonz_capE' simp:invs'_def valid_state'_def) apply (drule(1) sym_refs_ko_atD') apply (clarsimp elim!: ko_wp_at'_weakenE
                   intro!: refs_of_live') apply (clarsimp split del: if_split)+ apply (frule ko_at_valid_objs', clarsimp) apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def split del: if_split) apply (frule invs_sym') apply (drule(1) sym_refs_obj_atD') apply (clarsimp split del: if_split cong: if_cong
                         simp: st_tcb_at_refs_of_rev' ep_redux_simps' ntfn_bound_refs'_def) apply (frule st_tcb_at_state_refs_ofD') apply (erule delta_sym_refs) apply (fastforce simp: split: if_split_asm) apply (fastforce simp: tcb_bound_refs'_def set_eq_subset symreftype_inverse'
                      split: if_split_asm) apply (clarsimp simp:invs'_def) apply (frule ko_at_valid_objs') apply (clarsimp simp: valid_pspace'_def valid_state'_def) apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def split del: if_split) apply (clarsimp simp:invs'_def valid_state'_def valid_pspace'_def) apply (frule(1) ko_at_valid_objs') apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def
                  split: list.splits option.splits) apply (case_tac "ntfnBoundTCB nTFN", simp_all) apply (wp set_ntfn_minor_invs') apply (fastforce simp: valid_ntfn'_def invs'_def valid_state'_def
                    elim!: obj_at'_weakenE
                    dest!: global'_no_ex_cap) apply (wp add: hoare_convert_imp [OF asUser_nosch]
             hoare_convert_imp [OF setMRs_sch_act]
             setThreadState_nonqueued_state_update sts_st_tcb'
             del: cancelIPC_simple) apply (clarsimp | wp cancelIPC_ct')+ apply (wp set_ntfn_minor_invs' gts_wp' | clarsimp)+ apply (frule pred_tcb_at') by (wp set_ntfn_minor_invs'
        | rule conjI
        | clarsimp elim!: st_tcb_ex_cap''
        | fastforce simp: receiveBlocked_def projectKOs pred_tcb_at'_def obj_at'_def
                   dest!: invs_rct_ct_activatable'
                   split: thread_state.splits
        | fastforce simp: invs'_def valid_state'_def receiveBlocked_def projectKOs
                          valid_obj'_def valid_ntfn'_def
                   split: thread_state.splits
                   dest!: global'_no_ex_cap st_tcb_ex_cap'' ko_at_valid_objs')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_nonz_cap_to' ntfnptr\<rbrace> sendSignal ntfnptr badge \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_nonz_cap_to' ntfnptr\<rbrace> do nTFN <- getNotification ntfnptr;
case (ntfnObj nTFN, ntfnBoundTCB nTFN) of (Structures_H.ntfn.IdleNtfn, None) \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN | (Structures_H.ntfn.IdleNtfn, Some tcb) \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN
od | (Structures_H.ntfn.ActiveNtfn badge', x) \<Rightarrow> do newBadge <- return (badge || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | (Structures_H.ntfn.WaitingNtfn [], x) \<Rightarrow> haskell_fail [] | (Structures_H.ntfn.WaitingNtfn (dest # queue), x) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_nonz_cap_to' ntfnptr\<rbrace> do nTFN <- getNotification ntfnptr;
case (ntfnObj nTFN, ntfnBoundTCB nTFN) of (Structures_H.ntfn.IdleNtfn, None) \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN | (Structures_H.ntfn.IdleNtfn, Some tcb) \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN
od | (Structures_H.ntfn.ActiveNtfn badge', x) \<Rightarrow> do newBadge <- return (badge || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | (Structures_H.ntfn.WaitingNtfn [], x) \<Rightarrow> haskell_fail [] | (Structures_H.ntfn.WaitingNtfn (dest # queue), x) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>nTFN. \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case (ntfnObj nTFN, ntfnBoundTCB nTFN) of (Structures_H.ntfn.IdleNtfn, None) \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN | (Structures_H.ntfn.IdleNtfn, Some tcb) \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN
od | (Structures_H.ntfn.ActiveNtfn badge', x) \<Rightarrow> do newBadge <- return (badge || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | (Structures_H.ntfn.WaitingNtfn [], x) \<Rightarrow> haskell_fail [] | (Structures_H.ntfn.WaitingNtfn (dest # queue), x) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x3. ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case x3 of [] \<Rightarrow> haskell_fail [] | dest # queue \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN x3. ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case x3 of [] \<Rightarrow> haskell_fail [] | dest # queue \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN list. ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn list \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case list of [] \<Rightarrow> haskell_fail [] | dest # queue \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN list a lista. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> do y <- setNotification ntfnptr (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN);
y <- setThreadState Structures_H.thread_state.Running a;
y <- asUser a (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo a
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN list a lista. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 nTFN list a lista\<rbrace> do y <- setNotification ntfnptr (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN);
y <- setThreadState Structures_H.thread_state.Running a;
y <- asUser a (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo a
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; (invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q10 nTFN list a lista s
 3. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN list a lista y. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?B14 nTFN list a lista y\<rbrace> setThreadState Structures_H.thread_state.Running a \<lbrace>\<lambda>ya s. invs' s \<and> tcb_at' a s \<and> st_tcb_at' runnable' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)\<rbrace>
 2. \<And>nTFN list a lista. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 nTFN list a lista\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) \<lbrace>?B14 nTFN list a lista\<rbrace>
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; (invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q10 nTFN list a lista s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista. ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista) \<Longrightarrow> \<lbrace>?B14 nTFN (a # lista) a lista ()\<rbrace> setThreadState Structures_H.thread_state.Running a \<lbrace>\<lambda>ya s. invs' s \<and> tcb_at' a s \<and> st_tcb_at' runnable' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)\<rbrace>
 2. \<And>nTFN list a lista. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 nTFN list a lista\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) \<lbrace>?B14 nTFN list a lista\<rbrace>
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; (invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q10 nTFN list a lista s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista. ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista) \<Longrightarrow> \<lbrace>?B14 nTFN (a # lista) a lista ()\<rbrace> setThreadState Structures_H.thread_state.Running a \<lbrace>\<lambda>ya s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' a s \<and> st_tcb_at' runnable' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)\<rbrace>
 2. \<And>nTFN list a lista. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 nTFN list a lista\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) \<lbrace>?B14 nTFN list a lista\<rbrace>
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; (invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr) s\<rbrakk> \<Longrightarrow> ?Q10 nTFN list a lista s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_pspace' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s \<and> tcb_at' a s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b) \<and> if_live_then_nonz_cap' s \<and> ex_nonz_cap_to' a s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_pspace' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s \<and> a \<noteq> ksIdleThread s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 8. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 9. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 10. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>nTFN lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (ksCurThread s # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> False
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 8. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 9. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 10. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>nTFN lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (ksCurThread s # lista); ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; ksSchedulerAction s = ResumeCurrentThread; valid_pspace' s; ct_in_state' activatable' s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> False
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 8. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 9. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 10. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 8. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 8. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 2. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 8. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 9. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 10. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 7. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 8. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 7. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>nTFN lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (ksIdleThread s # lista); valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> False
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 7. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 6. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 6. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 2. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 6. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 7. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 5. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 6. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> ko_wp_at' live' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; state_refs_of' s ntfnptr = refs_of' (injectKOS nTFN) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS nTFN). ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' live' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 2. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; sym_refs (state_refs_of' s)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; sym_refs (state_refs_of' s); \<exists>obj. obj = nTFN \<and> state_refs_of' s ntfnptr = refs_of' (injectKOS obj) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS obj). ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then ntfn_q_refs_of' (case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) \<union> ntfn_bound_refs' (ntfnBoundTCB nTFN) else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; sym_refs (state_refs_of' s); state_refs_of' s ntfnptr = insert (a, NTFNSignal) (set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}); st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr) a s; \<forall>x\<in>set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; sym_refs (state_refs_of' s); state_refs_of' s ntfnptr = insert (a, NTFNSignal) (set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}); st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr) a s; \<forall>x\<in>set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; \<exists>ts ntfnptra. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptra) a s \<and> state_refs_of' s a = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptra\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>b. if b = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if b = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s b)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN a lista s x y tp. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; state_refs_of' s ntfnptr = insert (a, NTFNSignal) (set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}); st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr) a s; \<forall>x\<in>set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; \<exists>ts ntfnptra. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptra) a s \<and> state_refs_of' s a = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptra; (y, tp) \<in> (if x = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if x = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s x); (y, tp) \<notin> state_refs_of' s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if y = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s y)
 2. \<And>nTFN a lista s x y tp. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; state_refs_of' s ntfnptr = insert (a, NTFNSignal) (set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}); st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr) a s; \<forall>x\<in>set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; \<exists>ts ntfnptra. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptra) a s \<and> state_refs_of' s a = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptra; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if x = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if y = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s y)
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s x y tp. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); invs' s; ex_nonz_cap_to' ntfnptr s; tcb_at' a s; \<forall>t\<in>set lista. tcb_at' t s; a \<notin> set lista; distinct lista; case ntfnBoundTCB nTFN of None \<Rightarrow> True | Some tcb \<Rightarrow> a = tcb \<and> lista = []; valid_bound_tcb' (ntfnBoundTCB nTFN) s; state_refs_of' s ntfnptr = insert (a, NTFNSignal) (set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}); st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr) a s; \<forall>x\<in>set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound}. case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; \<exists>ts ntfnptra. ts = Structures_H.thread_state.BlockedOnNotification ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptra) a s \<and> state_refs_of' s a = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptra; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if x = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = a then {r \<in> if a = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s a. snd r = TCBBound} else if y = ntfnptr then set lista \<times> {NTFNSignal} \<union> set_option (ntfnBoundTCB nTFN) \<times> {NTFNBound} else state_refs_of' s y)
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 3. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> tcb_at' a s
 4. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 5. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 2. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> tcb_at' a s
 3. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 4. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_state' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN list a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); list = a # lista; invs' s \<and> ex_nonz_cap_to' ntfnptr s \<and> ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN a lista s ko. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; projectKO_opt ko = Some nTFN\<rbrakk> \<Longrightarrow> injectKOS nTFN = ko
 2. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 3. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN a lista s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.WaitingNtfn (a # lista); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; valid_obj' (injectKOS nTFN) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnObj_update (\<lambda>_. case lista of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn lista) nTFN) s
 2. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>nTFN. ntfnObj nTFN = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> case ntfnBoundTCB nTFN of None \<Rightarrow> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) | Some tcb \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do y <- cancelIPC tcb;
y <- setThreadState Structures_H.thread_state.Running tcb;
y <- asUser tcb (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo tcb
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = None\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN a. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> do state <- getThreadState a;
if receiveBlocked state then do y <- cancelIPC a;
y <- setThreadState Structures_H.thread_state.Running a;
y <- asUser a (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo a
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN s. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = None; (invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr) s\<rbrakk> \<Longrightarrow> (invs' and obj_at' (\<lambda>ntfn. ntfn_q_refs_of' (ntfnObj ntfn) = ntfn_q_refs_of' (ntfnObj (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)) \<and> ntfn_bound_refs' (ntfnBoundTCB ntfn) = ntfn_bound_refs' (ntfnBoundTCB (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN))) ntfnptr and valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) and (\<lambda>s. live' (KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)) \<longrightarrow> ex_nonz_cap_to' ntfnptr s) and (\<lambda>s. ntfnptr \<noteq> ksIdleThread s)) s
 2. \<And>nTFN a. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> do state <- getThreadState a;
if receiveBlocked state then do y <- cancelIPC a;
y <- setThreadState Structures_H.thread_state.Running a;
y <- asUser a (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo a
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>nTFN a. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> do state <- getThreadState a;
if receiveBlocked state then do y <- cancelIPC a;
y <- setThreadState Structures_H.thread_state.Running a;
y <- asUser a (setRegister Notification_H.badgeRegister badge);
possibleSwitchTo a
od else setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN)
od \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>nTFN a state. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a; receiveBlocked state\<rbrakk> \<Longrightarrow> \<lbrace>?P'1599 nTFN a state\<rbrace> cancelIPC a \<lbrace>\<lambda>rv s. st_tcb_at' simple' a s \<and> (Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' a s) \<and> (a = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. a \<notin> set (ksReadyQueues s p)))) \<and> tcb_at' a s \<and> (if a = a then K (runnable' Structures_H.thread_state.Running) else st_tcb_at' runnable' a) s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)\<rbrace>
 2. \<And>nTFN a state. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a; \<not> receiveBlocked state\<rbrakk> \<Longrightarrow> \<lbrace>?R1573 nTFN a state\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>nTFN a. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> getThreadState a \<lbrace>\<lambda>state s. (receiveBlocked state \<longrightarrow> (tcb_at' a and invs') s \<and> ?P'1599 nTFN a state s) \<and> (\<not> receiveBlocked state \<longrightarrow> ?R1573 nTFN a state s)\<rbrace>
 4. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>nTFN a state. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a; \<not> receiveBlocked state\<rbrakk> \<Longrightarrow> \<lbrace>?R1573 nTFN a state\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>nTFN a. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> getThreadState a \<lbrace>\<lambda>state s. (receiveBlocked state \<longrightarrow> (tcb_at' a and invs') s \<and> True \<and> ex_nonz_cap_to' a s \<and> a \<noteq> ksIdleThread s \<and> tcb_at' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)) \<and> (\<not> receiveBlocked state \<longrightarrow> ?R1573 nTFN a state s)\<rbrace>
 3. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>nTFN a s st. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a; invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; st_tcb_at' ((=) st) a s\<rbrakk> \<Longrightarrow> (receiveBlocked st \<longrightarrow> tcb_at' a s \<and> ex_nonz_cap_to' a s \<and> a \<noteq> ksIdleThread s \<and> tcb_at' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)) \<and> (\<not> receiveBlocked st \<longrightarrow> obj_at' (\<lambda>ntfn. ntfn_q_refs_of' (ntfnObj ntfn) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB ntfn) = {(a, NTFNBound)}) ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) s \<and> ntfnptr \<noteq> ksIdleThread s)
 2. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>nTFN a s st. \<lbrakk>ntfnObj nTFN = Structures_H.ntfn.IdleNtfn; ntfnBoundTCB nTFN = Some a; invs' s; ex_nonz_cap_to' ntfnptr s; ko_at' nTFN ntfnptr s; st_tcb_at' ((=) st) a s; tcb_at' a s\<rbrakk> \<Longrightarrow> (receiveBlocked st \<longrightarrow> tcb_at' a s \<and> ex_nonz_cap_to' a s \<and> a \<noteq> ksIdleThread s \<and> tcb_at' a s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> a)) \<and> (\<not> receiveBlocked st \<longrightarrow> obj_at' (\<lambda>ntfn. ntfn_q_refs_of' (ntfnObj ntfn) = {} \<and> ntfn_bound_refs' (ntfnBoundTCB ntfn) = {(a, NTFNBound)}) ntfnptr s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN) s \<and> ntfnptr \<noteq> ksIdleThread s)
 2. \<And>nTFN x2. ntfnObj nTFN = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>invs' and ex_nonz_cap_to' ntfnptr and ko_at' nTFN ntfnptr\<rbrace> setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn (badge || x2)) nTFN) \<lbrace>\<lambda>y. invs'\<rbrace>