--- a/PrioG.thy	Fri Dec 18 19:13:19 2015 +0800
+++ b/PrioG.thy	Fri Dec 18 22:47:32 2015 +0800
@@ -2914,4 +2914,15 @@
   from the concise and miniature model of PIP given in PrioGDef.thy.
 *}
 
+lemma eq_dependants: "dependants (wq s) = dependants s"
+  by (simp add: s_dependants_abv wq_def)
+
+lemma next_th_unique: 
+  assumes nt1: "next_th s th cs th1"
+  and nt2: "next_th s th cs th2"
+  shows "th1 = th2"
+using assms by (unfold next_th_def, auto)
+
+
+ 
 end