--- a/Correctness.thy	Mon Mar 06 13:11:16 2017 +0000
+++ b/Correctness.thy	Thu Mar 16 13:20:46 2017 +0000
@@ -1255,6 +1255,30 @@
   finally show ?thesis .
 qed
 
+value "sublists [a,b,cThe]"
+
+theorem bound_priority_inversion:
+  "card { s' @ s | s'. s' \<in> set t \<and>  th \<notin> running (s'@s) } \<le> 
+          1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
+   (is "?L \<le> ?R")
+proof - 
+  let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
+  from occs_le[of ?Q t] 
+  have "?L \<le> (1 + length t) - occs ?Q t" by simp
+  also have "... \<le> ?R"
+  proof -
+    have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
+              \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")
+    proof -
+      have "?L1 = length (actions_of {th} t)" using actions_split by arith
+      also have "... \<le> ?R1" using actions_th_occs by simp
+      finally show ?thesis .
+    qed            
+    thus ?thesis by simp
+  qed
+  finally show ?thesis .
+qed
+
 end
 
 text {*