--- a/prio/ExtGG.thy	Sun Feb 12 14:58:47 2012 +0000
+++ b/prio/ExtGG.thy	Sun Feb 12 15:05:57 2012 +0000
@@ -37,6 +37,8 @@
 context highest_gen
 begin
 
+
+
 lemma lt_tm: "tm < length s"
   by (insert preced_tm_lt[OF threads_s preced_th], simp)
 
@@ -118,6 +120,8 @@
 context extend_highest_gen
 begin
 
+thm extend_highest_gen_axioms_def
+
 lemma red_moment:
   "extend_highest_gen s th prio tm (moment i t)"
   apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
@@ -888,6 +892,15 @@
   show ?thesis by auto
 qed
 
+lemma runing_inversion_3:
+  assumes runing': "th' \<in> runing (t@s)"
+  and neq_th: "th' \<noteq> th"
+  shows "(th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
+proof -
+  from runing_inversion_2 [OF runing'] and neq_th
+  show ?thesis by auto
+qed
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto