188   inherited from the maximum of all its dependants, i.e. the threads which are waiting 

   188   inherited from the maximum of all its dependants, i.e. the threads which are waiting 

   189   directly or indirectly waiting for some resources from it. If no such thread exits, 

   189   directly or indirectly waiting for some resources from it. If no such thread exits, 

   190   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 

   190   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 

   191   @{text "preced th s"}.

   191   @{text "preced th s"}.

   192   *}

   192   *}

   193 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

   194 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

   195 

   196 

   196 (*<*)

   197 (*<*)

   197 lemma 

   198 lemma 

   198   cpreced_def2:

   199   cpreced_def2:

   199   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"

   200   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"