--- a/PrioG.thy	Wed Feb 03 21:51:57 2016 +0800
+++ b/PrioG.thy	Wed Feb 03 22:17:29 2016 +0800
@@ -1,5 +1,5 @@
-theory PrioG
-imports CpsG
+theory Correctness
+imports PIPBasics
 begin
 
 text {* 
@@ -580,6 +580,7 @@
   -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
   interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
   interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
+  interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto)
   show ?case
   proof -
     -- {* It can be proved that @{term cntP}-value of @{term th'} does not change
@@ -591,8 +592,8 @@
       -- {* 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_t.actor_inv[OF Cons(2)]
-      -- {* According to @{thm actor_inv}, @{term th'} must be running at 
+      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)
       -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
@@ -609,7 +610,7 @@
     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_t.actor_inv[OF Cons(2)]
+      with vat_es.actor_inv
       have "th' \<in> runing (t@s)" by (cases e, auto)
       moreover have "th' \<notin> runing (t@s)"
           using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .