theory IpcCancel_R

lemma cancelSignal_corres:
  "corres dc
          (invs and st_tcb_at ((=) (Structures_A.BlockedOnNotification ntfn)) t)
          (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) t)
          (cancel_signal t ntfn)
          (cancelSignal t ntfn)" apply (simp add: cancel_signal_def cancelSignal_def Let_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getNotification_corres]) apply (rule_tac F="isWaitingNtfn (ntfnObj ntfnaa)" in corres_gen_asm2) apply (case_tac "ntfn_obj ntfna") apply (simp add: ntfn_relation_def isWaitingNtfn_def) apply (simp add: isWaitingNtfn_def ntfn_relation_def split del: if_split) apply (rename_tac list) apply (rule_tac R="remove1 t list = []" in corres_cases) apply (simp del: dc_simp) apply (rule corres_split[OF setNotification_corres]) apply (simp add: ntfn_relation_def) apply (rule setThreadState_corres) apply simp apply (wp)+ apply (simp add: list_case_If del: dc_simp) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv) apply (rule setThreadState_corres) apply simp apply (wp)+ apply (simp add: isWaitingNtfn_def ntfn_relation_def) apply (wp getNotification_wp)+ apply (clarsimp simp: conj_comms st_tcb_at_tcb_at) apply (clarsimp simp: st_tcb_at_def obj_at_def) apply (erule pspace_valid_objsE) apply fastforce apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def) apply (drule sym, simp add: obj_at_def) apply (clarsimp simp: conj_comms pred_tcb_at' cong: conj_cong) apply (rule conjI) apply (simp add: pred_tcb_at'_def) apply (drule obj_at_ko_at') apply clarsimp apply (frule ko_at_valid_objs') apply fastforce apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_tcb'_def valid_tcb_state'_def) apply (drule sym, simp) apply (clarsimp simp: invs_weak_sch_act_wf) apply (drule sym_refs_st_tcb_atD', fastforce) apply (fastforce simp: isWaitingNtfn_def ko_wp_at'_def obj_at'_def projectKOs
                         ntfn_bound_refs'_def
                  split: Structures_H.notification.splits ntfn.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) (cancel_signal t ntfn) (cancelSignal t ntfn) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) (do ntfna <- get_notification ntfn;
queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ntfna <- get_notification ntfn;
queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ntfna ntfnaa. ntfn_relation ntfna ntfnaa \<Longrightarrow> corres dc (?R4 ntfna) (?R'4 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 5. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfna ntfnaa. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa)\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'10 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 4. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 5. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfna ntfnaa. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x2. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 4. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'10 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 6. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 7. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfna ntfnaa x2. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'10 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 5. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 6. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfna ntfnaa x2. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t x2)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t x2 of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'10 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 5. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 6. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?R4 ntfna) (?P'10 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'10 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 5. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 6. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> corres dc (?P14 ntfna) (?P'16 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?P14 ntfna and ?Q15 ntfna) (?P'16 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 4. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfn. ?P14 ntfn and ?Q15 ntfn\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'16 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 6. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 7. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> corres dc (?P14 ntfna) (?P'16 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn);
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?P14 ntfna and ?Q15 ntfna) (?P'16 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 4. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfn. ?P14 ntfn and ?Q15 ntfn\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ?P'16 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 6. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 7. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>ntfn ntfna list. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna)
 2. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R19 ntfn ntfna list y) (?R'19 ntfn ntfna list rv') (set_thread_state t Structures_A.thread_state.Inactive) (setThreadState Structures_H.thread_state.Inactive t)
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>?R19 ntfna ntfnaa list\<rbrace>
 4. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>?R'19 ntfna ntfnaa list\<rbrace>
 5. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 6. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna) (ntfn_at' ntfn and ?Q'24 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 7. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and ?Q'24 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 9. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 10. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R19 ntfn ntfna list y) (?R'19 ntfn ntfna list rv') (set_thread_state t Structures_A.thread_state.Inactive) (setThreadState Structures_H.thread_state.Inactive t)
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>?R19 ntfna ntfnaa list\<rbrace>
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>?R'19 ntfna ntfnaa list\<rbrace>
 4. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 5. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna) (ntfn_at' ntfn and ?Q'24 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 6. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and ?Q'24 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 8. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 9. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []; dc y rv'\<rbrakk> \<Longrightarrow> thread_state_relation Structures_A.thread_state.Inactive Structures_H.thread_state.Inactive
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>y. tcb_at t\<rbrace>
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>rv'. tcb_at' t\<rbrace>
 4. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 5. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna) (ntfn_at' ntfn and ?Q'24 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 6. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and ?Q'24 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 8. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 9. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q22 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna Structures_A.ntfn.IdleNtfn) \<lbrace>\<lambda>y. tcb_at t\<rbrace>
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfnaa) \<lbrace>\<lambda>rv'. tcb_at' t\<rbrace>
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 4. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna) (ntfn_at' ntfn and ?Q'24 ntfnaa and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 5. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and ?Q22 ntfna and ?Q15 ntfna\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and ?Q'24 ntfna and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 7. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 8. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do ntfn' <- case remove1 t list of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and ?Q15 ntfna) (ntfn_at' ntfn and tcb_at' t and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and ?Q15 ntfna\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 5. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 6. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfna) (?Q'17 ntfnaa) (do y <- set_notification ntfn (ntfn_set_obj ntfna (Structures_A.ntfn.WaitingNtfn (remove1 t list)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and ?Q15 ntfna) (ntfn_at' ntfn and tcb_at' t and ?Q'17 ntfnaa) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 3. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and ?Q15 ntfna\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and ?Q'17 ntfna and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 5. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 6. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>ntfn ntfna list. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj ntfn (Structures_A.ntfn.WaitingNtfn (remove1 t list))) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfna)
 2. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R41 ntfn ntfna list y) (?R'41 ntfn ntfna list rv') (set_thread_state t Structures_A.thread_state.Inactive) (setThreadState Structures_H.thread_state.Inactive t)
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (Structures_A.ntfn.WaitingNtfn (remove1 t list))) \<lbrace>?R41 ntfna ntfnaa list\<rbrace>
 4. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfnaa) \<lbrace>?R'41 ntfna ntfnaa list\<rbrace>
 5. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)) (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfnaa)) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 6. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfna) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 8. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 9. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []; dc y rv'\<rbrakk> \<Longrightarrow> corres dc (?R41 ntfn ntfna list y) (?R'41 ntfn ntfna list rv') (set_thread_state t Structures_A.thread_state.Inactive) (setThreadState Structures_H.thread_state.Inactive t)
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (Structures_A.ntfn.WaitingNtfn (remove1 t list))) \<lbrace>?R41 ntfna ntfnaa list\<rbrace>
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfnaa) \<lbrace>?R'41 ntfna ntfnaa list\<rbrace>
 4. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)) (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfnaa)) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 5. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfna) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 7. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 8. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn ntfna list y rv'. \<lbrakk>ntfnObj ntfna = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna; ntfn_obj ntfn = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []; dc y rv'\<rbrakk> \<Longrightarrow> thread_state_relation Structures_A.thread_state.Inactive Structures_H.thread_state.Inactive
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (Structures_A.ntfn.WaitingNtfn (remove1 t list))) \<lbrace>\<lambda>y. tcb_at t\<rbrace>
 3. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfnaa) \<lbrace>\<lambda>rv'. tcb_at' t\<rbrace>
 4. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)) (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfnaa)) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 5. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfna) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 7. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 8. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 ntfna\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (Structures_A.ntfn.WaitingNtfn (remove1 t list))) \<lbrace>\<lambda>y. tcb_at t\<rbrace>
 2. \<And>ntfna ntfnaa list. \<lbrakk>ntfnObj ntfnaa = Structures_H.ntfn.WaitingNtfn list \<and> ntfn_bound_tcb ntfna = ntfnBoundTCB ntfnaa; ntfn_obj ntfna = Structures_A.ntfn.WaitingNtfn list; remove1 t list \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 ntfnaa\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (remove1 t list)) ntfnaa) \<lbrace>\<lambda>rv'. tcb_at' t\<rbrace>
 3. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)) (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfnaa)) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 4. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and ?Q44 ntfna)\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and ?Q'46 ntfna) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 6. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 7. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfna ntfnaa x3. \<lbrakk>ntfn_relation ntfna ntfnaa; isWaitingNtfn (ntfnObj ntfnaa); ntfn_obj ntfna = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and tcb_at t)) (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t)) (do queue <- case ntfn_obj ntfna of Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 t queue)));
set_thread_state t Structures_A.thread_state.Inactive
od) (do y <- assert (case ntfnObj ntfnaa of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfnaa)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfnaa))) (ntfnObj ntfnaa);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfnaa);
setThreadState Structures_H.thread_state.Inactive t
od)
 2. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and tcb_at t)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 4. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 5. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_notification ntfn \<lbrace>\<lambda>ntfna. ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and tcb_at t)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getNotification ntfn \<lbrace>\<lambda>ntfna. ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))\<rbrace>
 3. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and ?Q4) s
 4. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at ntfn and (ntfn_at ntfn and tcb_at t and (ntfn_at ntfn and tcb_at t))) s
 2. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs s; st_tcb_at ((=) (Structures_A.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> ntfn_at ntfn s
 2. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; kheap s t = Some (TCB tcb); Structures_A.thread_state.BlockedOnNotification ntfn = tcb_state tcb\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ntfn = Some ko \<and> is_ntfn ko
 2. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; Structures_A.thread_state.BlockedOnNotification ntfn = tcb_state tcb\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s tcb. \<lbrakk>invs s; Structures_A.thread_state.BlockedOnNotification ntfn = tcb_state tcb; kheap s t = Some (TCB tcb); valid_obj t (TCB tcb) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ntfn = Some ko \<and> is_ntfn ko
 3. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; Structures_A.thread_state.BlockedOnNotification ntfn = tcb_state tcb; kheap s t = Some (TCB tcb); valid_obj t (TCB tcb) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ntfn = Some ko \<and> is_ntfn ko
 2. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>invs s; Structures_A.thread_state.BlockedOnNotification ntfn = tcb_state tcb; kheap s t = Some (TCB tcb); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr t (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); case tcb_state tcb of Structures_A.thread_state.BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | Structures_A.thread_state.BlockedOnSend ref sp \<Rightarrow> ep_at ref s | Structures_A.thread_state.BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True; case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s ntfn = Some ko \<and> is_ntfn ko
 2. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t) s \<Longrightarrow> (ntfn_at' ntfn and (\<lambda>s. \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (ntfn_at' ntfn and tcb_at' t and (ntfn_at' ntfn and tcb_at' t) and (\<lambda>s. isWaitingNtfn (ntfnObj ntfna))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s \<and> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs' s; obj_at' (\<lambda>ko. Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko) t s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs' s; \<exists>ko. ko_at' ko t s \<and> Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (4 subgoals):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s ko koa. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> injectKO ko = koa
 3. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 4. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (3 subgoals):
 1. \<And>s ko koa. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> injectKO ko = koa
 2. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 3. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>invs' s; ko_at' ko t s; Structures_H.thread_state.BlockedOnNotification ntfn = tcbState ko; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF ko)) s; case tcbState ko of Structures_H.thread_state.BlockedOnReceive ref a \<Rightarrow> ep_at' ref s | Structures_H.thread_state.BlockedOnNotification ref \<Rightarrow> ntfn_at' ref s | Structures_H.thread_state.BlockedOnSend ref a b d c \<Rightarrow> ep_at' ref s | _ \<Rightarrow> True; is_aligned (tcbIPCBuffer ko) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification ko) s; tcbDomain ko \<le> maxDomain; tcbPriority ko \<le> maxPriority; tcbMCP ko \<le> maxPriority\<rbrakk> \<Longrightarrow> ntfn_at' ntfn s
 2. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfna. \<lbrakk>invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) t s; ko_at' ntfna ntfn s\<rbrakk> \<Longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfna. \<lbrakk>invs' s; ko_at' ntfna ntfn s; \<exists>ts ntfnptr. Structures_H.thread_state.BlockedOnNotification ntfn = ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (t, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> isWaitingNtfn (ntfnObj ntfna) proof (prove)
goal:
No subgoals!