--- a/PrioG.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/PrioG.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -2269,6 +2269,20 @@
 qed
 
 
+lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+apply(subgoal_tac "finite (runing s)")
+prefer 2
+apply (metis finite_nat_set_iff_bounded lessI runing_unique)
+apply(case_tac "Suc (Suc 0) \<le> card (runing s)")
+apply(subst (asm) card_le_Suc_iff)
+apply(simp)
+apply(auto)[1]
+apply (metis insertCI runing_unique)
+apply(auto) 
+done
+  
+
+
 lemma create_pre:
   assumes stp: "step s e"
   and not_in: "th \<notin> threads s"