--- a/Correctness.thy	Fri Feb 12 12:32:57 2016 +0800
+++ b/Correctness.thy	Fri Feb 12 17:50:24 2016 +0800
@@ -589,13 +589,11 @@
     proof(rule ccontr) -- {* Proof by contradiction. *}
       -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}
       assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"
-      -- {* Then the actor of @{term e} must be @{term th'} and @{term e}
-            must be a @{term P}-event: *}
-      hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) 
-      with vat_es.actor_inv
-      -- {* According to @{thm vat_es.actor_inv}, @{term th'} must be running at 
-            the moment @{term "t@s"}: *}
-      have "th' \<in> runing (t@s)" by (cases e, auto)
+      from cntP_diff_inv[OF this[simplified]]
+      obtain cs' where "e = P th' cs'" by auto
+      from vat_es.pip_e[unfolded this]
+      have "th' \<in> runing (t@s)" 
+        by (cases, simp)
       -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
             shows @{term th'} can not be running at moment  @{term "t@s"}: *}
       moreover have "th' \<notin> runing (t@s)" 
@@ -609,9 +607,10 @@
     moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'"
     proof(rule ccontr) -- {* Proof by contradiction. *}
       assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"
-      hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) 
-      with vat_es.actor_inv
-      have "th' \<in> runing (t@s)" by (cases e, auto)
+      from cntV_diff_inv[OF this[simplified]]
+      obtain cs' where "e = V th' cs'" by auto
+      from vat_es.pip_e[unfolded this]
+      have "th' \<in> runing (t@s)" by (cases, auto)
       moreover have "th' \<notin> runing (t@s)"
           using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
       ultimately show False by simp