--- a/PIPBasics.thy	Wed Aug 24 16:13:20 2016 +0200
+++ b/PIPBasics.thy	Sun Oct 02 14:32:05 2016 +0100
@@ -3336,11 +3336,9 @@
 context valid_trace
 begin
 
-text {*
-  The first lemma is technical, which says out of any node 
-  in the domain of @{term RAG},
-  (no matter whether it is thread node or resource node)  
-  there is a path leading to a ready thread.
+text {* The first lemma is technical, which says out of any node in the
+domain of @{term RAG} (no matter whether it is thread node or resource
+node), there is a path leading to a ready thread.
 *}
 
 lemma chain_building:
@@ -3409,12 +3407,15 @@
 
 lemma th_chain_to_ready_tG:
   assumes th_in: "th \<in> threads s"
-  shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (th, th') \<in> (tG s)^+)"
+  shows "\<exists>th'\<in> nancestors (tG s) th. th' \<in> readys s"
 proof -
   from th_chain_to_ready[OF assms]
   show ?thesis
-  using dependants_alt_def1 dependants_alt_tG by blast 
-qed
+  using dependants_alt_def1 dependants_alt_tG 
+  unfolding nancestors_def ancestors_def
+  by blast 
+qed
+
 
 text {*
   The following lemma is a technical one to show