--- a/Correctness.thy	Thu Mar 16 13:20:46 2017 +0000
+++ b/Correctness.thy	Fri Mar 17 14:57:30 2017 +0000
@@ -1255,30 +1255,6 @@
   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 {*