theory Finalise_C

lemma unbindMaybeNotification_ccorres:
  "ccorres dc xfdc (invs') (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) []
        (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)" supply option.case_cong[cong] apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) apply (rule_tac P="ntfnBoundTCB ntfn \<noteq> None \<longrightarrow>
                         option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL"
             in ccorres_gen_asm) apply (rule_tac xf'=boundTCB_'
                and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)"
                and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)"
             in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1[OF cmap_relation_ntfn]) apply (erule ko_at_projectKO_opt) apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) apply ceqv apply wpc apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip) apply (rule ccorres_cond_true) apply (rule ccorres_call[where xf'=xfdc]) apply (rule doUnbindNotification_ccorres'[simplified]) apply simp apply simp apply simp apply (clarsimp simp add: guard_is_UNIV_def option_to_ctcb_ptr_def ) apply (wp getNotification_wp) apply (clarsimp ) apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) by (auto simp: valid_ntfn'_def valid_bound_tcb'_def obj_at'_def projectKOs
                      objBitsKO_def is_aligned_def option_to_ctcb_ptr_def tcb_at_not_NULL
             split: ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace>) [] (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace>) [] (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> ccorres dc xfdc (?Q116 ntfnPtr) (?Q'116 ntfnPtr) [SKIP] (do ntfn <- getNotification ntfnptr;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od) (\<acute>ret__unsigned :== CALL notification_ptr_get_ntfnBoundTCB_'proc(ntfnPtr);;
(\<acute>boundTCB :== tcb_Ptr \<acute>ret__unsigned;;
IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI))
 2. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> ?Q'116 ntfnPtr proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr ntfn. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> ccorres dc xfdc (?Q122 ntfnPtr ntfn) (?Q'122 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (\<acute>ret__unsigned :== CALL notification_ptr_get_ntfnBoundTCB_'proc(ntfnPtr);;
(\<acute>boundTCB :== tcb_Ptr \<acute>ret__unsigned;;
IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI))
 2. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>?Q122 ntfnPtr\<rbrace>
 3. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q122 ntfnPtr rv s \<longrightarrow> s' \<in> ?Q'122 ntfnPtr rv} proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr ntfn. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> ccorres dc xfdc (?Q122 ntfnPtr ntfn) (?Q'122 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (\<acute>ret__unsigned :== CALL notification_ptr_get_ntfnBoundTCB_'proc(ntfnPtr);;
\<acute>boundTCB :== tcb_Ptr \<acute>ret__unsigned;;
IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI)
 2. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>?Q122 ntfnPtr\<rbrace>
 3. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q122 ntfnPtr rv s \<longrightarrow> s' \<in> ?Q'122 ntfnPtr rv} proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G131 ntfnPtr ntfn) (?Q'122 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (\<acute>ret__unsigned :== CALL notification_ptr_get_ntfnBoundTCB_'proc(ntfnPtr);;
\<acute>boundTCB :== tcb_Ptr \<acute>ret__unsigned;;
IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI)
 2. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?G131 ntfnPtr ntfn and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 3. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?G131 ntfnPtr rv and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> ?Q'122 ntfnPtr rv} proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr ntfn s. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) s \<and> (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL notification_ptr_get_ntfnBoundTCB_'proc(ntfnPtr);;
\<acute>boundTCB :== tcb_Ptr \<acute>ret__unsigned ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>boundTCB = option_to_ctcb_ptr (ntfnBoundTCB ntfn)\<rbrace>)
 2. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 5. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 6. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfn s. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL \<Longrightarrow> UNIV \<inter> {s'. (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) s \<and> (s, s') \<in> rf_sr} \<subseteq> {sa. sa \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>ret__unsigned. ret__unsigned = ntfnBoundTCB_CL (notification_lift (the (cslift sa (ntfn_Ptr ntfnptr)))) \<longrightarrow> (s, boundTCB_'_update (\<lambda>_. tcb_Ptr (ntfnBoundTCB_CL (notification_lift (the (cslift sa (ntfn_Ptr ntfnptr)))))) (sa\<lparr>ret__unsigned_' := ntfnBoundTCB_CL (notification_lift (the (cslift sa (ntfn_Ptr ntfnptr))))\<rparr>)) \<in> rf_sr \<and> tcb_Ptr (ntfnBoundTCB_CL (notification_lift (the (cslift sa (ntfn_Ptr ntfnptr))))) = option_to_ctcb_ptr (ntfnBoundTCB ntfn))}
 2. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 5. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 6. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfn s x. \<lbrakk>(\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ko_at' ntfn ntfnptr s; valid_bound_tcb' (ntfnBoundTCB ntfn) s; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> tcb_Ptr (ntfnBoundTCB_CL (notification_lift (the (cslift x (ntfn_Ptr ntfnptr))))) = option_to_ctcb_ptr (ntfnBoundTCB ntfn)
 2. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 5. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 6. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn s x. \<lbrakk>(\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ko_at' ntfn ntfnptr s; valid_bound_tcb' (ntfnBoundTCB ntfn) s\<rbrakk> \<Longrightarrow> map_to_ntfns (ksPSpace s) (?x160 ntfn s x) = Some (?y160 ntfn s x)
 2. \<And>ntfn s x y'. \<lbrakk>(\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ko_at' ntfn ntfnptr s; valid_bound_tcb' (ntfnBoundTCB ntfn) s; map_to_ntfns (ksPSpace s) (?x160 ntfn s x) = Some (?y160 ntfn s x); cnotification_relation (cslift x) (?y160 ntfn s x) y'; cslift x (ntfn_Ptr (?x160 ntfn s x)) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> tcb_Ptr (ntfnBoundTCB_CL (notification_lift (the (cslift x (ntfn_Ptr ntfnptr))))) = option_to_ctcb_ptr (ntfnBoundTCB ntfn)
 3. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 5. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 6. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 7. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfn s x y'. \<lbrakk>(\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ko_at' ntfn ntfnptr s; valid_bound_tcb' (ntfnBoundTCB ntfn) s; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift x) ntfn y'; cslift x (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> tcb_Ptr (ntfnBoundTCB_CL (notification_lift (the (cslift x (ntfn_Ptr ntfnptr))))) = option_to_ctcb_ptr (ntfnBoundTCB ntfn)
 2. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 5. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 6. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ceqv \<Gamma> boundTCB_' rv' t t' (IF \<acute>boundTCB \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,\<acute>boundTCB)
FI) (?y'132 ntfnPtr ntfn rv')
 2. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (?y'132 ntfnPtr ntfn (option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 4. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 5. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P132 ntfnPtr ntfn) (?Q132 ntfnPtr ntfn) [SKIP] (case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od) (IF option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn))
FI)
 2. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. ?Q132 ntfnPtr ntfn)
 3. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. ?P132 ntfnPtr ntfn and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 4. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P132 ntfnPtr rv and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R212 ntfnPtr ntfn) (?R''214 ntfnPtr ntfn) [SKIP] (return ()) (IF option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn))
FI)
 2. \<And>ntfnPtr ntfn x2. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R213 ntfnPtr ntfn x2) (?R''215 ntfnPtr ntfn x2) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None x2
od) (IF option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn))
FI)
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> ?R''214 ntfnPtr ntfn} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> ?R''215 ntfnPtr ntfn x}})
 4. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> ?R212 ntfnPtr ntfn s) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R213 ntfnPtr ntfn x s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 5. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> ?R212 ntfnPtr rv s) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> ?R213 ntfnPtr rv x s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R212 ntfnPtr ntfn) (?R'217 ntfnPtr ntfn) [SKIP] (return ()) SKIP
 2. \<And>ntfnPtr ntfn x2. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R213 ntfnPtr ntfn x2) (?R''215 ntfnPtr ntfn x2) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None x2
od) (IF option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn))
FI)
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> ?R'217 ntfnPtr ntfn \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> ?R''215 ntfnPtr ntfn x}})
 4. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> ?R212 ntfnPtr ntfn s) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R213 ntfnPtr ntfn x s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 5. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> ?R212 ntfnPtr rv s) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> ?R213 ntfnPtr rv x s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr ntfn x2. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R213 ntfnPtr ntfn x2) (?R''215 ntfnPtr ntfn x2) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None x2
od) (IF option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn))
FI)
 2. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> ?R''215 ntfnPtr ntfn x}})
 3. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R213 ntfnPtr ntfn x s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 4. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> ?R213 ntfnPtr rv x s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr ntfn x2. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R213 ntfnPtr ntfn x2) (?R'220 ntfnPtr ntfn x2) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None x2
od) (CALL doUnbindNotification_'proc(ntfnPtr,option_to_ctcb_ptr (ntfnBoundTCB ntfn)))
 2. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> ?R'220 ntfnPtr ntfn x \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 3. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R213 ntfnPtr ntfn x s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 4. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> ?R213 ntfnPtr rv x s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfnPtr ntfn x2. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres dc (?xf''222 ntfnPtr ntfn x2) (?R213 ntfnPtr ntfn x2) (?C'222 ntfnPtr ntfn x2) [] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None x2
od) (Call doUnbindNotification_'proc)
 2. \<And>ntfnPtr ntfn x2 s ta sa. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals sa = globals sa
 3. \<And>ntfnPtr ntfn x2 a s t. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = ?xf''222 ntfnPtr ntfn x2 t
 4. \<And>ntfnPtr ntfn x2 s. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals (tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s)) = globals s
 5. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> {s. tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s) \<in> ?C'222 ntfnPtr ntfn x} \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 6. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> ?R213 ntfnPtr ntfn x s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 7. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> ?R213 ntfnPtr rv x s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr ntfn x2 s ta sa. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals sa = globals sa
 2. \<And>ntfnPtr ntfn x2 a s t. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = xfdc t
 3. \<And>ntfnPtr ntfn x2 s. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals (tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s)) = globals s
 4. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> {s. tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcb_ptr_to_ctcb_ptr x\<rbrace>} \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 5. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 6. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr ntfn x2 a s t. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> xfdc (s\<lparr>globals := globals t\<rparr>) = xfdc t
 2. \<And>ntfnPtr ntfn x2 s. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals (tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s)) = globals s
 3. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> {s. tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcb_ptr_to_ctcb_ptr x\<rbrace>} \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 4. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 5. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr ntfn x2 s. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL; ntfnBoundTCB ntfn = Some x2\<rbrakk> \<Longrightarrow> globals (tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s)) = globals s
 2. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> {s. tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcb_ptr_to_ctcb_ptr x\<rbrace>} \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 3. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 4. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = option_to_ctcb_ptr (ntfnBoundTCB ntfn)) boundTCB_' (\<lambda>rv rv'. {s. ntfnBoundTCB ntfn = None \<longrightarrow> s \<in> UNIV \<inter> - \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. ntfnBoundTCB ntfn = Some x \<longrightarrow> s \<in> {s. tcbptr_'_update (\<lambda>_. option_to_ctcb_ptr (ntfnBoundTCB ntfn)) (ntfnPtr_'_update (\<lambda>_. ntfnPtr) s) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcb_ptr_to_ctcb_ptr x\<rbrace>} \<inter> \<lbrace>option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL\<rbrace>}})
 2. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 3. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr. ntfnPtr = ntfn_Ptr ntfnptr \<Longrightarrow> \<lbrace>?Q116 ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. (\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)\<rbrace>
 2. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfn. ko_at' ntfn ntfnptr s \<longrightarrow> ((\<lambda>s. (ntfnBoundTCB ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' ntfn ntfnptr) s)) and (ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)) and (\<lambda>_. ntfnBoundTCB ntfn \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)) s) \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. (ntfnBoundTCB rv = None \<longrightarrow> True) \<and> (\<forall>x. ntfnBoundTCB rv = Some x \<longrightarrow> (invs' and tcb_at' x and ko_at' rv ntfnptr) s)) and (ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)) and (\<lambda>_. ntfnBoundTCB rv \<noteq> None \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL)) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>s s' ntfn. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ko_at' ntfn ntfnptr s\<rbrakk> \<Longrightarrow> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> tcb_at' x s) \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ntfn. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ko_at' ntfn ntfnptr s; valid_ntfn' ntfn s\<rbrakk> \<Longrightarrow> (\<forall>x. ntfnBoundTCB ntfn = Some x \<longrightarrow> tcb_at' x s) \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s \<and> ((\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL)