624   before reaching state @{text "s"}.

   624   before reaching state @{text "s"}.

   625   *}

   625   *}

   626 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"

   626 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"

   627   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"

   627   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"

   628 

   628 

   629 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

   631 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

   630        difference is the order of arguemts. *}

   632        difference is the order of arguemts. *}

   631 definition "the_preced s th = preced th s"

   633 definition "the_preced s th = preced th s"

   632 

   634 

   633 text {* @{term "the_thread"} extracts thread out of RAG node. *}

   635 text {* @{term "the_thread"} extracts thread out of RAG node. *}