789   "vt step (P th cs#s) \<Longrightarrow>

   789   "vt step (P th cs#s) \<Longrightarrow>

   790   depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}

   790   depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}

   791                                              else depend s \<union> {(Th th, Cs cs)})"

   791                                              else depend s \<union> {(Th th, Cs cs)})"

   792   apply(unfold s_depend_def wq_def)

   792   apply(unfold s_depend_def wq_def)

   793   apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)

   793   apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)

   795   apply(fold wq_def)

   795   apply(fold wq_def)

   796   apply(drule_tac step_back_step)

   796   apply(drule_tac step_back_step)

   799 

   800 

   800 lemma simple_A:

   801 lemma simple_A:

   801   fixes A

   802   fixes A

   802   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"

   803   assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"

   803   shows "A = {} \<or> (\<exists> a. A = {a})"

   804   shows "A = {} \<or> (\<exists> a. A = {a})"