--- a/PIPDefs.thy	Sun Jan 31 18:15:13 2016 +0800
+++ b/PIPDefs.thy	Mon Feb 01 20:56:39 2016 +0800
@@ -657,6 +657,11 @@
   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 
              s_holding_abv cs_RAG_def, auto)
 
+lemma tRAG_alt_def: 
+  "tRAG s = {(Th th1, Th th2) | th1 th2. 
+                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
+ by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
+
 definition "cp_gen s x =
                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"