--- a/Correctness.thy	Fri Oct 07 21:15:35 2016 +0100
+++ b/Correctness.thy	Fri Oct 21 14:47:01 2016 +0100
@@ -504,6 +504,9 @@
   assumes running': "th' \<in> running (t @ s)"
   shows "cp (t @ s) th' = preced th s"
 proof -
+  have "th' \<in> readys (t @ s)" using assms
+    using running_ready subsetCE by blast
+    
   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms
       unfolding running_def by simp
   also have "... =  Max (cp (t @ s) ` threads (t @ s))"