theory IpcCancel_C

lemma isStopped_ccorres [corres]:
  "ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
  (tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})  []
  (isStopped thread) (Call isStopped_'proc)" apply (cinit lift: thread_' simp: getThreadState_def) apply (rule ccorres_pre_threadGet) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_symb_exec_r) apply (rule ccorres_cond_weak) apply (rule ccorres_return_C) apply simp apply simp apply simp apply (simp add: ccorres_cond_iffs) apply (rule ccorres_return_C) apply simp apply simp apply simp apply vcg apply (rule conseqPre) apply vcg apply clarsimp apply clarsimp apply (clarsimp simp: typ_heap_simps ctcb_relation_thread_state_to_tsType
                 split: thread_state.splits) apply (simp add: "StrictC'_thread_state_defs")+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (tcb_at' thread) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (isStopped thread) (Call isStopped_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Q159 threada) (?Q'159 threada) [SKIP] (do state <- threadGet tcbState thread;
return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c threada} (\<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)
ELSE
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI)
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q159 threada s \<and> s' \<in> ?Q'159 threada proof (prove)
goal (2 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?P165 threada state) (?P'165 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c threada} (\<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)
ELSE
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI)
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P165 threada (tcbState tcb) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'165 threada (tcbState tcb)} proof (prove)
goal (2 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?A167 threada state) (?C'167 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (\<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)
ELSE
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI)
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (?A167 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?A167 threada state) (?Q'169 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)
ELSE
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI)
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (?Q'169 threada state)
 3. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ?A167 threada state s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (?A167 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pt173 threada state) (?Rt173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 threada state) (?Rf173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (?Rt173 threada state \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 4. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (?Pt173 threada state and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 5. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (?Pt173 threada (tcbState tcb) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ret__unsigned_long_' (global_exn_var_'_update f (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) true\<rparr>)) = SCAST(32 signed \<rightarrow> 32) true
 2. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 4. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 threada state) (?Rf173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 5. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 6. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 7. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 threada state) (?Rf173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 4. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 5. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 threada state) (?Rf173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 4. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 5. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 threada state) (?Rf173 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 3. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?Pf173 (tcb_ptr_to_ctcb_ptr thread) state) (?Rf173 (tcb_ptr_to_ctcb_ptr thread) state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True)) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 3. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and ?Pf173 threada state) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ret__unsigned_long_' (global_exn_var_'_update f (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) false\<rparr>)) = SCAST(32 signed \<rightarrow> 32) false
 2. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 4. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 5. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>threada state s f. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> globals (ret__unsigned_long_'_update f s) = globals s
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 3. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 4. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 5. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> wfhandlers [SKIP]
 2. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 3. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>threada state. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) (\<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrace>)
 2. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?C'167 threada state \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 3. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'167 threada (tcbState tcb) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'198 threada state s) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))) {s'. (s, s') \<in> rf_sr}
 2. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'198 threada state s
 3. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>threada state s. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; ((\<lambda>_. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. \<forall>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (s, sa\<lparr>ret__unsigned_' := tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C'']))))\<rparr>) \<in> rf_sr}
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True) and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned = tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) true) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) = to_bool (SCAST(32 signed \<rightarrow> 32) false) \<and> \<not> (tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(threada\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)\<rbrace> \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb ctcb t. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb; ctcb_relation tcb ctcb; ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))); (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive\<rbrakk> \<Longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> False | Structures_H.thread_state.IdleThreadState \<Rightarrow> False | Structures_H.thread_state.Restart \<Rightarrow> False | _ \<Rightarrow> True) \<and> (tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive \<or> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb ctcb t. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb; ctcb_relation tcb ctcb; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; tcbState tcb = Structures_H.thread_state.Running; ThreadState_Running = ThreadState_BlockedOnReply \<or> ThreadState_Running = ThreadState_BlockedOnNotification \<or> ThreadState_Running = ThreadState_BlockedOnSend \<or> ThreadState_Running = ThreadState_BlockedOnReceive \<or> ThreadState_Running = ThreadState_Inactive\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' tcb ctcb t. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb; ctcb_relation tcb ctcb; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState; idle' (tcbState tcb); ThreadState_IdleThreadState = ThreadState_BlockedOnReply \<or> ThreadState_IdleThreadState = ThreadState_BlockedOnNotification \<or> ThreadState_IdleThreadState = ThreadState_BlockedOnSend \<or> ThreadState_IdleThreadState = ThreadState_BlockedOnReceive \<or> ThreadState_IdleThreadState = ThreadState_Inactive\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' tcb ctcb t. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ctcb; ctcb_relation tcb ctcb; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart; tcbState tcb = Structures_H.thread_state.Restart; ThreadState_Restart = ThreadState_BlockedOnReply \<or> ThreadState_Restart = ThreadState_BlockedOnNotification \<or> ThreadState_Restart = ThreadState_BlockedOnSend \<or> ThreadState_Restart = ThreadState_BlockedOnReceive \<or> ThreadState_Restart = ThreadState_Inactive\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!