3784   using vt assms next_th_holding next_th_waiting

  3784   using vt assms next_th_holding next_th_waiting

  3785   by (unfold s_RAG_def, simp)

  3785   by (unfold s_RAG_def, simp)

  3786 

  3786 

  3787 end

  3787 end

  3788 

  3788 

  3789 -- {* A useless definition *}

  3790 -- {* A useless definition *}

  3790 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"

  3791 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"

  3791 where "cps s = {(th, cp s th) | th . th \<in> threads s}"

  3792 where "cps s = {(th, cp s th) | th . th \<in> threads s}"

  3792 

  3793 

  3793 end

  3794 end