--- a/Implementation.thy	Sun Feb 07 21:21:53 2016 +0800
+++ b/Implementation.thy	Mon Feb 08 10:57:01 2016 +0800
@@ -81,7 +81,7 @@
         (is "Max (?f ` ?S1) = Max (?g ` ?S2)")
   proof -
     -- {* The base sets are equal. *}
-    have "?S1 = ?S2" using RAG_unchanged by simp
+    have "?S1 = ?S2" using RAG_es by simp
     -- {* The function values on the base set are equal as well. *}
     moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"
     proof
@@ -163,6 +163,14 @@
   to take over the critical resource released by the initiating thread @{text "th"}.
 *}
 
+lemma (in valid_trace_v)
+  the_preced_es: "the_preced (e#s) = the_preced s"
+proof
+  fix th'
+  show "the_preced (e # s) th' = the_preced s th'"
+    by (unfold the_preced_def preced_def is_v, simp)
+qed
+
 context valid_trace_v_n
 begin
 
@@ -375,7 +383,7 @@
 
 lemma tRAG_s: 
   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
-  using local.RAG_tRAG_transfer[OF RAG_es cs_held] .
+  using RAG_tRAG_transfer[OF RAG_es cs_held] .
 
 lemma cp_kept:
   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
@@ -561,7 +569,7 @@
 begin 
 
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
-  by (unfold tRAG_alt_def RAG_unchanged, auto)
+  by (unfold tRAG_alt_def RAG_es, auto)
 
 lemma preced_kept:
   assumes "th' \<noteq> th"
@@ -634,7 +642,7 @@
   by (unfold the_preced_def is_exit preced_def, simp)
 
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
-  by (unfold tRAG_alt_def RAG_unchanged, auto)
+  by (unfold tRAG_alt_def RAG_es, auto)
 
 lemma th_RAG: "Th th \<notin> Field (RAG s)"
 proof -