--- a/prio/ExtGG.thy	Mon Feb 13 10:44:42 2012 +0000
+++ b/prio/ExtGG.thy	Mon Feb 13 10:57:47 2012 +0000
@@ -892,15 +892,39 @@
   show ?thesis by auto
 qed
 
+lemma runing_preced_inversion:
+  assumes runing': "th' \<in> runing (t@s)"
+  shows "cp (t@s) th' = preced th s"
+proof -
+  from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))"
+    by (unfold runing_def, auto)
+  also have "\<dots> = preced th s"
+  proof -
+    from max_cp_readys_threads[OF vt_t]
+    have "\<dots> =  Max (cp (t @ s) ` threads (t @ s))" .
+    also have "\<dots> = preced th s"
+    proof -
+      from max_kept
+      and max_cp_eq [OF vt_t]
+      show ?thesis by auto
+    qed
+    finally show ?thesis .
+  qed
+  finally show ?thesis .
+qed
+
 lemma runing_inversion_3:
   assumes runing': "th' \<in> runing (t@s)"
   and neq_th: "th' \<noteq> th"
-  shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
+  shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
 proof -
-  from runing_inversion_2 [OF runing'] and neq_th
+  from runing_inversion_2 [OF runing'] 
+    and neq_th 
+    and runing_preced_inversion[OF runing']
   show ?thesis by auto
 qed
 
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto