--- a/PIPBasics.thy	Sat Feb 06 23:42:03 2016 +0800
+++ b/PIPBasics.thy	Sun Feb 07 21:21:53 2016 +0800
@@ -2047,9 +2047,14 @@
 subsection {* Uniqueness of waiting *}
 
 text {*
-  Uniqueness of waiting is expressed by the following
-  predicate over system state (or event trace).
-  It says a thread can only be blocked on one resource.
+  {\em Uniqueness of waiting} means that 
+  a thread can only be blocked on one resource.
+  This property is needed in order to prove that @{term RAG}
+  is acyclic. Therefore, we need to prove it first in the following
+  lemma @{text "waiting_unqiue"}, all lemmas before it are auxiliary. 
+
+  The property is expressed by the following predicate over system 
+  state (or event trace), which is also named @{text "waiting_unqiue"}.
 *}
 
 definition 
@@ -2064,7 +2069,8 @@
 *}
 
 text {*
-  As a first step, we need to understand how 
+  As a first step to prove lemma @{text "waiting_unqiue"}, 
+  we need to understand how 
   a thread is get blocked. 
   We show in the following lemmas 
   (all named @{text "waiting_inv"}) that 
@@ -2151,7 +2157,7 @@
 proof -
   from assms(2)
   show ?thesis
-  by (cases rule:waiting_esE, insert assms, auto)
+  by (cases rule:waiting_esE, insert assms, auto) (* ccc *)
 qed
 
 end
@@ -2171,7 +2177,6 @@
 
 end
 
-
 context valid_trace_e
 begin
 
@@ -2217,6 +2222,13 @@
   qed
 qed
 
+text {* 
+  Now, with @{thm waiting_inv} in place, the following lemma
+  shows the uniqueness of waiting is kept by every operation 
+  in the PIP protocol. This lemma constitutes the main part
+  in the proof of lemma @{text "waiting_unique"}.
+*}
+
 lemma waiting_unique_kept:
   assumes "waiting_unique s"
   shows "waiting_unique (e#s)"
@@ -2262,6 +2274,12 @@
 context valid_trace
 begin
 
+text {*
+  With @{thm valid_trace_e.waiting_unique_kept} in place,
+  the proof of the following lemma @{text "waiting_unique"} 
+  needs only a very simple induction.
+*}
+
 lemma waiting_unique 
   [unfolded waiting_unique_def, rule_format]:
   shows "waiting_unique s"
@@ -2278,8 +2296,16 @@
 
 end
 
+
 subsection {* Acyclic keeping *}
 
+text {*
+  To prove that @{term RAG} is acyclic, we need to show the acyclic property 
+  is preserved by all system operations. There are only two non-trivial cases, 
+  the @{term P} and @{term V} operation, where are treated in the following
+  locales, under the name @{text "acylic_RAG_kept"}:
+*}
+
 context valid_trace_v_e
 begin 
 
@@ -2402,6 +2428,12 @@
 context valid_trace
 begin
 
+text {* 
+  With these @{text "acylic_RAG_kept"}-lemmas proved, 
+  the proof of the following @{text "acyclic_RAG"} is
+  straight forward. 
+ *}
+
 lemma acyclic_RAG:
   shows "acyclic (RAG s)"
 proof(induct rule:ind)
@@ -2467,6 +2499,12 @@
 
 section {* RAG is single-valued *}
 
+text {*
+  The proof that @{term RAG} is single-valued makes use of 
+  @{text "unique_waiting"} and @{thm held_unique} and the
+  proof itself is very simple:
+*}
+
 context valid_trace
 begin