--- a/Correctness.thy	Wed Jan 06 16:34:26 2016 +0000
+++ b/Correctness.thy	Thu Jan 07 08:33:13 2016 +0800
@@ -1,5 +1,5 @@
 theory Correctness
-imports PIPBasics Implementation
+imports PIPBasics
 begin
 
 text {* 
@@ -467,7 +467,7 @@
   a thread is running or not.
 *}
 
-lemma pv_blocked_pre:
+lemma pv_blocked_pre: (* ddd *)
   assumes th'_in: "th' \<in> threads (t@s)"
   and neq_th': "th' \<noteq> th"
   and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
@@ -496,7 +496,7 @@
 
 lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
 
-lemma runing_precond_pre:
+lemma runing_precond_pre: (* ddd *)
   fixes th'
   assumes th'_in: "th' \<in> threads s"
   and eq_pv: "cntP s th' = cntV s th'"
@@ -600,7 +600,7 @@
 lemmas runing_precond_pre_dtc = runing_precond_pre
          [folded vat_t.detached_eq vat_s.detached_eq]
 
-lemma runing_precond:
+lemma runing_precond: (* ddd *)
   fixes th'
   assumes th'_in: "th' \<in> threads s"
   and neq_th': "th' \<noteq> th"
@@ -660,7 +660,7 @@
           moment_plus_split neq_th' th'_in)
 qed
 
-lemma moment_blocked_eqpv:
+lemma moment_blocked_eqpv: (* ddd *)
   assumes neq_th': "th' \<noteq> th"
   and th'_in: "th' \<in> threads ((moment i t)@s)"
   and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
@@ -830,7 +830,6 @@
   apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
   by (metis neq_th runing' runing_inversion_3)
 
-
 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'"}