--- a/prio/ExtGG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/ExtGG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -952,6 +952,20 @@
   show ?thesis by auto
 qed
 
+lemma runing_inversion_4:
+  assumes runing': "th' \<in> runing (t@s)"
+  and neq_th: "th' \<noteq> th"
+  shows "th' \<in> threads s"
+  and    "\<not>detached s th'"
+  and    "cp (t@s) th' = preced th s"
+using runing_inversion_3 [OF runing'] 
+  and neq_th 
+  and runing_preced_inversion[OF runing']
+apply(auto simp add: detached_eq[OF vt_s])
+done
+
+
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto