--- a/PIPBasics.thy	Fri Oct 07 14:05:08 2016 +0100
+++ b/PIPBasics.thy	Fri Oct 07 21:15:35 2016 +0100
@@ -3629,8 +3629,13 @@
   are disjoint.
 *}
 
+lemma subtree_RAG_tG: 
+  shows "subtree (tG s) th = {th'. Th th' \<in> subtree (RAG s) (Th th)}"
+  using subtree_tG_tRAG threads_set_eq by auto
+
+
 lemma threads_alt_def:
-  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+  "threads s = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
     (is "?L = ?R")
 proof -
   { fix th1
@@ -3658,6 +3663,10 @@
   } ultimately show ?thesis by auto
 qed
 
+lemma threads_alt_def1:
+  shows "(threads s) = (\<Union> th \<in> readys s. subtree (tG s) th)"
+unfolding threads_alt_def subtree_RAG_tG  ..
+
 lemma readys_subtree_disjoint:
   assumes "th1 \<in> readys s"
   and "th2 \<in> readys s"
@@ -3812,27 +3821,24 @@
   over the union of subtrees, the following equation can be derived:
 *}
 
-lemma max_cp_readys_max_preced:
+thm the_preced_def cpreceds_def
+
+lemma max_cp_readys_max_preced_tG:
   shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
 proof(cases "readys s = {}")
   case False
   have "?R = 
-    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-    by (simp add: threads_alt_def)  
-  also have "... = 
-    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-          by (unfold image_UN, simp)
-  also have "... = 
-    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
+    Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))"
+    by (simp add: threads_alt_def1)  
+  also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) "
+    by (unfold image_UN, simp)
+  also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" 
   proof(rule Max_UNION)
-    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
-                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
-                        using finite_subtree_threads by auto
+    show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M"
+      using fsbttGs.finite_subtree by auto
   qed (auto simp:False subtree_def finite_readys)
-  also have "... = 
-     Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` 
-                        readys s)" 
-      by (simp add: image_comp)
+  also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)"
+    by (simp add: image_comp)
   also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
   proof -
     have "(?f ` ?A) = (?g ` ?A)"
@@ -3840,20 +3846,21 @@
       fix th1 
       assume "th1 \<in> ?A"
       thus "?f th1 = ?g th1"
-        by (unfold cp_alt_def, simp)
+        by (unfold cp_alt_def2, simp)
     qed
     thus ?thesis by simp
   qed
   finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
 
+
 text {*
-  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
+  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
   and @{thm max_cp_eq}:
 *}
 lemma max_cp_readys_threads:
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
-    using max_cp_readys_max_preced max_cp_eq by auto
+    using max_cp_readys_max_preced_tG max_cp_eq by auto
 
 end