--- a/Test.thy	Fri May 30 07:56:39 2014 +0100
+++ b/Test.thy	Mon Jun 02 14:58:42 2014 +0100
@@ -350,7 +350,70 @@
 qed (simp_all)
 
 
+lemma finite_RAG:
+  assumes "vt s"
+  shows "finite (RAG2 s)"
+using assms
+apply(induct)
+apply(simp add: RAG2_def RAG_def waits_def holds_def)
+apply(erule step.cases)
+apply(auto)
+apply(case_tac "wq sa cs = []")
+apply(rule finite_subset)
+apply(rule RAG_p1)
+apply(simp)
+apply(simp)
+apply(rule finite_subset)
+apply(rule RAG_p2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "\<exists>wts. wq sa cs = th # wts")
+apply(erule exE)
+apply(case_tac "wts = []")
+apply(rule finite_subset)
+apply(rule RAG_v1)
+apply(simp)
+apply(simp)
+apply(rule finite_subset)
+apply(rule RAG_v2)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(subgoal_tac "th \<in> set (wq sa cs) \<and> th = hd (wq sa cs)") 
+apply(case_tac "wq sa cs") 
+apply(auto)[2]
+apply(auto simp add: holds2_def holds_def wq_def)
+done
+
+lemma wq_threads: 
+  assumes vt: "vt s"
+  and h: "th \<in> set (wq s cs)"
+  shows "th \<in> threads s"
+using assms
+apply(induct)
+apply(simp add: wq_def)
+apply(erule step.cases)
+apply(auto simp add: wq_def Let_def holding_def holds2_def holds_def waits2_def runing_def readys_def)
+apply(simp add: waits_def)
+apply(auto simp add: waits_def split: if_splits)[1]
+apply(auto split: if_splits)
+apply(simp only: waits_def)
+by (metis insert_iff set_simps(2))
+
+lemma max_cpreceds_readys_threads:
+  assumes vt: "vt s"
+  shows "Max (cpreceds2 s (readys s)) = Max (cpreceds2 s (threads s))"
+apply(case_tac "threads s = {}")
+apply(simp add: readys_def)
+using vt
+apply(induct)
+apply(simp)
+apply(erule step.cases)
+apply(auto simp add: readys_def waits2_def waits_def Let_def holding_def runing_def holds2_def)
+defer
+defer
+oops
 
 
-
-
+end
\ No newline at end of file