theory IpcCancel_C

lemma isRunnable_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})  []
  (isRunnable thread) (Call isRunnable_'proc)" apply (cinit lift: thread_' simp: getThreadState_def) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_pre_threadGet) 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>) [] (isRunnable thread) (Call isRunnable_'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)
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_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running 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. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_' (?A165 threada) (?C'165 threada) [SKIP] (do state <- threadGet tcbState thread;
return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)
od) (\<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_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running 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> (?A165 threada and tcb_at' (ctcb_ptr_to_tcb_ptr threada)) s \<and> s' \<in> ?C'165 threada \<inter> \<lbrace>True\<rbrace> 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_' (?P167 threada state) (?P'167 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (\<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_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running 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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P167 threada (tcbState tcb) s) 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> ?P'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_' (?P167 threada state) (?Q'169 threada state) [SKIP] (return (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running 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> (?P'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; ?P167 threada state s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P167 threada (tcbState tcb) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> (?Pt173 threada (tcbState tcb) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)) (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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> ?Rf173 threada state \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and ?Pf173 threada (tcbState tcb)) s) 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> ?P'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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> ?P'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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> ?P'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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> ?P'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> (?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) true)\<rbrace> \<inter> \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrace> \<union> \<lbrace>(case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = to_bool (SCAST(32 signed \<rightarrow> 32) false)\<rbrace> \<inter> - \<lbrace>\<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<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> (?P'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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> ?P'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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> ((\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s) 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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running) \<or> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) = 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_Restart \<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_Running)\<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> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<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_Restart \<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_Running\<rbrakk> \<Longrightarrow> (case tcbState tcb of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) \<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_Restart \<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_Running) proof (prove)
goal (6 subgoals):
 1. \<And>s s' tcb ctcb t x11 x12 x12a. \<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_BlockedOnReceive; tcbState tcb = Structures_H.thread_state.BlockedOnReceive x11 x12; ThreadState_BlockedOnReceive = ThreadState_Restart \<or> ThreadState_BlockedOnReceive = ThreadState_Running\<rbrakk> \<Longrightarrow> x12 = (\<not> x12a)
 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_BlockedOnReply; awaiting_reply' (tcbState tcb); ThreadState_BlockedOnReply = ThreadState_Restart \<or> ThreadState_BlockedOnReply = ThreadState_Running\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' tcb ctcb t x3. \<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_BlockedOnNotification; tcbState tcb = Structures_H.thread_state.BlockedOnNotification x3; ThreadState_BlockedOnNotification = ThreadState_Restart \<or> ThreadState_BlockedOnNotification = ThreadState_Running\<rbrakk> \<Longrightarrow> False
 4. \<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_Inactive; tcbState tcb = Structures_H.thread_state.Inactive; ThreadState_Inactive = ThreadState_Restart \<or> ThreadState_Inactive = ThreadState_Running\<rbrakk> \<Longrightarrow> False
 5. \<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_Restart \<or> ThreadState_IdleThreadState = ThreadState_Running\<rbrakk> \<Longrightarrow> False
 6. \<And>s s' tcb ctcb t x71 x72 x74 x73a x75a x74a. \<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_BlockedOnSend; tcbState tcb = Structures_H.thread_state.BlockedOnSend x71 x72 x73a x74 x75a; ThreadState_BlockedOnSend = ThreadState_Restart \<or> ThreadState_BlockedOnSend = ThreadState_Running\<rbrakk> \<Longrightarrow> x74 = (\<not> x74a) proof (prove)
goal:
No subgoals!