--- a/Correctness.thy	Mon Dec 19 23:43:54 2016 +0000
+++ b/Correctness.thy	Mon Feb 06 12:27:20 2017 +0000
@@ -725,35 +725,11 @@
 
 section {* The existence of `blocking thread` *}
 
-text {* 
-  Suppose @{term th} is not running, it is first shown that
-  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
-  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
-
-  Now, since @{term readys}-set is non-empty, there must be
-  one in it which holds the highest @{term cp}-value, which, by definition, 
-  is the @{term running}-thread. However, we are going to show more: this 
-  running thread is exactly @{term "th'"}. *}
-
-
-lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
-                    "th' \<in> running (t @ s)"
+lemma th_ancestor_has_max_ready:
+  assumes th'_in: "th' \<in> readys (t@s)" 
+  and dp: "th' \<in> nancestors (tG (t @ s)) th"
+  shows "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
 proof -
-    -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
-       ready ancestor of @{term th}. *}
-  have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 
-    using th_kept vat_t.th_chain_to_ready_tG by auto
-  then obtain th' where th'_in: "th' \<in> readys (t@s)"
-                    and dp: "th' \<in> nancestors (tG (t @ s)) th"
-    by blast
-
-  -- {* We are going to first show that this @{term th'} is running. *}
-  have "th' \<in> running (t @ s)"
-  proof -
-    -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}
-    have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")
-    proof -
       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
             the  @{term cp}-value of @{term th'} is the maximum of 
             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
@@ -776,14 +752,40 @@
         using th_cp_max th_cp_preced th_kept 
               the_preced_def vat_t.max_cp_readys_threads by auto
       finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
-    qed 
+ qed 
+
+
+text {* 
+  Suppose @{term th} is not running, it is first shown that
+  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
+  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
+
+  Now, since @{term readys}-set is non-empty, there must be
+  one in it which holds the highest @{term cp}-value, which, by definition, 
+  is the @{term running}-thread. However, we are going to show more: this 
+  running thread is exactly @{term "th'"}. *}
+
 
-    -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
-          it is @{term running} by definition. *}
-    with `th' \<in> readys (t @ s)` 
-    show "th' \<in> running (t @ s)" by (simp add: running_def) 
-  qed
+lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
+  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
+                    "th' \<in> running (t @ s)"
+proof -
+    -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
+       ready ancestor of @{term th}. *}
+  have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 
+    using th_kept vat_t.th_chain_to_ready_tG by auto
+  then obtain th' where th'_in: "th' \<in> readys (t @ s)"
+                    and dp: "th' \<in> nancestors (tG (t @ s)) th"
+    by blast
 
+  -- {* We are going to first show that this @{term th'} is running. *}
+
+  from th'_in dp
+  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" 
+    by (rule th_ancestor_has_max_ready)
+  with `th' \<in> readys (t @ s)` 
+  have "th' \<in> running (t @ s)" by (simp add: running_def) 
+ 
   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
   moreover have "th' \<in> nancestors (tG (t @ s)) th"
     using dp unfolding nancestors_def2 by simp
@@ -931,15 +933,15 @@
   thus ?thesis unfolding blockers_def by simp
 qed
 
-text {*
-  The following lemma shows that a blocker may never die
-  as long as the highest thread @{term th} is living. 
+text {* The following lemma shows that a blocker does not die as long as the
+highest thread @{term th} is live.
 
-  The reason for this is that, before a thread can execute an @{term Exit} operation,
-  it must give up all its resource. However, the high priority inherited by a blocker 
-  thread also goes with the resources it once held, and the consequence is the lost of 
-  right to run, the other precondition for it to execute its own  @{term Exit} operation.
-  For this reason, a blocker may never exit before the exit of the highest thread @{term th}.
+  The reason for this is that, before a thread can execute an @{term Exit}
+  operation, it must give up all its resource. However, the high priority
+  inherited by a blocker thread also goes with the resources it once held,
+  and the consequence is the lost of right to run, the other precondition
+  for it to execute its own @{term Exit} operation. For this reason, a
+  blocker may never exit before the exit of the highest thread @{term th}.
 *}
 
 lemma blockers_kept: