[STATEMENT]
lemma step_thread_Some_NoneD:
  assumes det: "\<alpha>.deterministic I"
  and step: "step_thread update_state s t' = \<lfloor>(t, None, \<sigma>')\<rfloor>"
  and invar: "state_invar s" "state_\<alpha> s \<in> I"
  shows "\<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> ln $ n > 0 \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> 0 < ln $ n \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)
[PROOF STEP]
using assms step_thread_correct(1)[OF det _ invar(1), of "\<lambda>_ _. True", of id update_state t']
[PROOF STATE]
proof (prove)
using this:
\<alpha>.deterministic I
step_thread update_state s t' = \<lfloor>(t, None, \<sigma>')\<rfloor>
state_invar s
state_\<alpha> s \<in> I
\<lbrakk>True; state_\<alpha> s \<in> I\<rbrakk> \<Longrightarrow> map_option (apsnd (apsnd id)) (step_thread update_state s t') = \<alpha>.step_thread (id \<circ> update_state) (state_\<alpha> s) t'

goal (1 subgoal):
 1. \<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> 0 < ln $ n \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)
[PROOF STEP]
by(fastforce simp add: map_option.id dest: \<alpha>.step_thread_Some_NoneD[OF sym])