--- a/PIPDefs.thy~	Sun Jan 17 22:18:35 2016 +0800
+++ b/PIPDefs.thy~	Wed Jan 27 19:26:56 2016 +0800
@@ -626,6 +626,8 @@
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
 
+definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))"
+
 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
        difference is the order of arguemts. *}
 definition "the_preced s th = preced th s"