--- a/PIPBasics.thy	Fri Feb 05 20:11:12 2016 +0800
+++ b/PIPBasics.thy	Sat Feb 06 08:35:45 2016 +0800
@@ -1185,18 +1185,31 @@
 section {* The change of @{term RAG} *}
 
 text {*
+  The whole of PIP resides on the understanding of the formation
+  of @{term RAG}. In this section, we are going to investigate how
+  @{term RAG} is changed with the execution of every event (or operation).
+  The effect of every event on @{text RAG} is derived in its respective
+  locale named @{text "RAG_es"} with all lemmas before auxiliary. 
+
+  The derivation of these @{text "RAG_es"}s forms the very basis 
+  to show the well-formedness of @{term RAG}, 
+  for example, @{term RAG} is finite, acyclic, and single-valued, etc.
+
+*}
+
+text {*
   The following three lemmas show that @{text "RAG"} does not change
   by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
   events, respectively.
 *}
 
-lemma (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
+lemma (in valid_trace_set) RAG_es [simp]: "(RAG (e # s)) = RAG s"
    by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)
 
-lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
+lemma (in valid_trace_create) RAG_es [simp]: "(RAG (e # s)) = RAG s"
  by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)
 
-lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s"
+lemma (in valid_trace_exit) RAG_es[simp]: "(RAG (e # s)) = RAG s"
   by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)
 
 context valid_trace_v
@@ -1701,24 +1714,6 @@
  qed
 qed
 
-lemma 
-  finite_RAG_kept:
-  assumes "finite (RAG s)"
-  shows "finite (RAG (e#s))"
-proof(cases "rest = []")
-  case True
-  interpret vt: valid_trace_v_e using True
-    by (unfold_locales, simp)
-  show ?thesis using assms
-    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
-next
-  case False
-  interpret vt: valid_trace_v_n using False
-    by (unfold_locales, simp)
-  show ?thesis using assms
-    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
-qed
-
 end
 
 context valid_trace_p
@@ -1981,6 +1976,29 @@
 
 section {* RAG is finite *}
 
+context valid_trace_v
+begin
+
+lemma 
+  finite_RAG_kept:
+  assumes "finite (RAG s)"
+  shows "finite (RAG (e#s))"
+proof(cases "rest = []")
+  case True
+  interpret vt: valid_trace_v_e using True
+    by (unfold_locales, simp)
+  show ?thesis using assms
+    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
+next
+  case False
+  interpret vt: valid_trace_v_n using False
+    by (unfold_locales, simp)
+  show ?thesis using assms
+    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
+qed
+
+end
+
 context valid_trace
 begin