[STATEMENT]
lemma deadlockedAcquire_must_wait:
  "\<And>ln. \<lbrakk> thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); ln $ l > 0; must_wait s t (Inl l) (deadlocked s \<union> final_threads s) \<rbrakk>
  \<Longrightarrow> t \<in> deadlocked s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; must_wait s t (Inl l) (deadlocked s \<union> final_threads s)\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply(erule must_wait_elims)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ln la t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 2. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inl t'); not_final_thread s t'; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 3. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inr t'); all_final_except s (deadlocked s \<union> final_threads s); t' \<notin> interrupts s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply(erule (2) deadlockedAcquire)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> has_lock (locks s $ l) (?t'4 ln la t')
 2. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> ?t'4 ln la t' \<noteq> t
 3. \<And>ln la t'. \<lbrakk>\<not> waiting (wset s t); 0 < ln $ l; Inl l = Inl la; has_lock (locks s $ la) t'; t' \<noteq> t; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> ?t'4 ln la t' \<in> deadlocked s \<or> ?t'4 ln la t' \<in> final_threads s
 4. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inl t'); not_final_thread s t'; t' \<in> deadlocked s \<union> final_threads s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
 5. \<And>ln t'. \<lbrakk>thr s t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s t); 0 < ln $ l; Inl l = Inr (Inr t'); all_final_except s (deadlocked s \<union> final_threads s); t' \<notin> interrupts s\<rbrakk> \<Longrightarrow> t \<in> deadlocked s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done