--- a/PIPBasics.thy	Fri Jun 09 15:08:54 2017 +0100
+++ b/PIPBasics.thy	Fri Jun 23 00:27:16 2017 +0100
@@ -3136,6 +3136,8 @@
 
 end
 
+
+
 text {*
   It can be shown that @{term tRAG} is also a 
   finite-branch relational tree (or forest):  
@@ -5463,6 +5465,7 @@
   qed
 qed
 
+
 lemma readys_RAG:
   assumes "th \<in> readys s"
   shows "Th th \<notin> Domain (RAG s)"
@@ -5478,6 +5481,36 @@
   qed
 qed
 
+
+text {*
+  The following two lemmas are general about any valid system state, 
+  but are used in the derivation in more specific system operations. 
+*}
+
+lemma readys_root:
+  assumes "th \<in> readys s"
+  shows "root (RAG s) (Th th)"
+  unfolding root_def ancestors_def
+  using readys_RAG assms
+by (metis Collect_empty_eq Domain.DomainI trancl_domain)
+
+lemma readys_in_no_subtree:
+  assumes "th \<in> readys s"
+  and "th' \<noteq> th"
+  shows "Th th \<notin> subtree (RAG s) (Th th')" 
+proof
+   assume "Th th \<in> subtree (RAG s) (Th th')"
+   thus False
+   proof(cases rule:subtreeE)
+      case 1
+      with assms show ?thesis by auto
+   next
+      case 2
+      with readys_root[OF assms(1)]
+      show ?thesis by (auto simp:root_def)
+   qed
+qed
+
 lemma readys_holdents_detached:
   assumes "th \<in> readys s"
   and "holdents s th = {}"