--- a/prio/ExtGG.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/ExtGG.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -546,7 +546,7 @@
     by auto
 qed
 
-lemma pv_blocked:
+lemma pv_blocked_pre:
   fixes th'
   assumes th'_in: "th' \<in> threads (t@s)"
   and neq_th': "th' \<noteq> th"
@@ -584,6 +584,8 @@
   qed
 qed
 
+lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]]
+
 lemma runing_precond_pre:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
@@ -695,6 +697,8 @@
 qed
 *)
 
+lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]]
+
 lemma runing_precond:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
@@ -708,7 +712,7 @@
     from runing_precond_pre[OF th'_in eq_pv neq_th']
     have h1: "th' \<in> threads (t @ s)"  
       and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
-    from pv_blocked[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .
+    from pv_blocked_pre[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .
     with is_runing show "False" by simp
   qed
   moreover from cnp_cnv_cncs[OF vt_s, of th'] 
@@ -812,7 +816,7 @@
   from assms show ?case by auto
 qed
 
-lemma moment_blocked:
+lemma moment_blocked_eqpv:
   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'"
@@ -828,6 +832,24 @@
   show ?thesis by auto
 qed
 
+lemma moment_blocked:
+  assumes neq_th': "th' \<noteq> th"
+  and th'_in: "th' \<in> threads ((moment i t)@s)"
+  and dtc: "detached (moment i t @ s) th'"
+  and le_ij: "i \<le> j"
+  shows "detached (moment j t @ s) th' \<and>
+         th' \<in> threads ((moment j t)@s) \<and>
+         th' \<notin> runing ((moment j t)@s)"
+proof -
+  from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s]
+  have vt_i: "vt (moment i t @ s)" by auto
+  from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s]
+  have vt_j: "vt  (moment j t @ s)" by auto
+  from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij, 
+  folded detached_eq[OF vt_j]]
+  show ?thesis .
+qed
+
 lemma runing_inversion_1:
   assumes neq_th': "th' \<noteq> th"
   and runing': "th' \<in> runing (t@s)"
@@ -877,7 +899,7 @@
   from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp
   with eq_me [symmetric]
   have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp
-  from moment_blocked [OF neq_th' h2 h1, of "length t"] and lt_its
+  from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its
   and moment_ge
   have "th' \<notin> runing (t @ s)" by auto
   with runing'
@@ -924,7 +946,6 @@
   show ?thesis by auto
 qed
 
-
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto
@@ -1002,3 +1023,4 @@
 end
 
 
+