diff -r b620a2a0806a -r b4bcd1edbb6d PrioGDef.thy~
--- a/PrioGDef.thy~	Wed Jan 06 20:46:14 2016 +0800
+++ b/PrioGDef.thy~	Wed Jan 06 16:34:26 2016 +0000
@@ -1,4 +1,4 @@
- {* Definitions *}
+chapter {* Definitions *}
 (*<*)
 theory PrioGDef
 imports Precedence_ord Moment
@@ -387,6 +387,8 @@
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
   where "cp s \<equiv> cprec_fun (schs s)"
 
+definition "cp_gen s x = Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+
 text {* \noindent
   Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 
   @{text "dependants"} still have the 
@@ -585,6 +587,7 @@
   *}
 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
   where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> 
+                                     t = hd (SOME q. distinct q \<and> set q = set rest))"
 
 text {* \noindent
   The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}